module Data.Partial.Properties where
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