open import 1Lab.Prelude

open import Data.Partial.Base
module Data.Partial.Properties where
private variable
  o o' β„“ : Level
  A B C : Type β„“

abstract

Properties of partial elementsπŸ”—

This module establishes some elementary properties of partial elements, and the information ordering on them. First, as long as is a set, the information ordering is an actual poset:

  βŠ‘-refl : {x : β†― A} β†’ x βŠ‘ x
  βŠ‘-refl .implies x-def = x-def
  βŠ‘-refl .refines _     = refl

  βŠ‘-trans : {x y z : β†― A} β†’ x βŠ‘ y β†’ y βŠ‘ z β†’ x βŠ‘ z
  βŠ‘-trans p q .implies = q .implies ∘ p .implies
  βŠ‘-trans {x = x} {y} {z} p q .refines x-def =
    z .elt _ β‰‘βŸ¨ q .refines (p .implies x-def) ⟩
    y .elt _ β‰‘βŸ¨ p .refines x-def ⟩
    x .elt _ ∎

  βŠ‘-antisym : {x y : β†― A} β†’ x βŠ‘ y β†’ y βŠ‘ x β†’ x ≑ y
  βŠ‘-antisym {x = x} {y = y} p q = part-ext (p .implies) (q .implies) Ξ» xd yd β†’
    β†―-indep x βˆ™ q .refines yd

We actually have that never is the bottom element, as claimed:

  never-βŠ‘ : {x : β†― A} β†’ never βŠ‘ x
  never-βŠ‘ .implies ()
  never-βŠ‘ .refines ()

Our mapping operation preserves ordering, is functorial, and preserves the bottom element:

  part-map-βŠ‘
    : βˆ€ {f : A β†’ B} {x y : β†― A}
    β†’ x βŠ‘ y β†’ part-map f x βŠ‘ part-map f y
  part-map-βŠ‘         p .implies   = p .implies
  part-map-βŠ‘ {f = f} p .refines d = ap f (p .refines d)

  part-map-id : βˆ€ (x : β†― A) β†’ part-map (Ξ» a β†’ a) x ≑ x
  part-map-id x = part-ext id id Ξ» _ _ β†’
    β†―-indep x

  part-map-∘
    : βˆ€ (f : B β†’ C) (g : A β†’ B)
    β†’ βˆ€ (x : β†― A) β†’ part-map (f ∘ g) x ≑ part-map f (part-map g x)
  part-map-∘ f g x = part-ext id id Ξ» _ _ β†’
    ap (f ∘ g) (β†―-indep x)

  part-map-never : βˆ€ {f : A β†’ B} {x} β†’ part-map f never βŠ‘ x
  part-map-never .implies ()
  part-map-never .refines ()

Finally, we can characterise the adjunction-unit-to-be, always.

  always-inj : {x y : A} β†’ always x ≑ always y β†’ x ≑ y
  always-inj {x = x} p =
    J (Ξ» y p β†’ (d : ⌞ y ⌟) β†’ x ≑ y .elt d) (Ξ» _ β†’ refl) p tt

  always-βŠ‘ : {x : β†― A} {y : A} β†’ (βˆ€ d β†’ x .elt d ≑ y) β†’ x βŠ‘ always y
  always-βŠ‘ p .implies _ = tt
  always-βŠ‘ p .refines d = sym (p d)

  always-βŠ’ : {x : A} {y : β†― A} β†’ y ↓ x β†’ always x βŠ‘ y
  always-βŠ’ (p , q) .implies _ = p
  always-βŠ’ (p , q) .refines _ = q

  always-natural : {x : A} (f : A β†’ B) β†’ part-map f (always x) ≑ always (f x)
  always-natural f = part-ext (Ξ» _ β†’ tt) (Ξ» _ β†’ tt) Ξ» _ _ β†’ refl