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