module Data.Power.Complemented where
Complemented subobjectsπ
A subobject of a type is called complemented if there is a subobject such that 1, and . Because of βs lattice structure, these containments suffice to establish equality.
is-complemented : β {β} {A : Type β} (p : β A) β Type _ is-complemented {A = A} p = Ξ£[ pβ»ΒΉ β β A ] ((p β© pβ»ΒΉ β minimal) Γ (maximal β p βͺ pβ»ΒΉ))
More conventionally, in constructive mathematics, we may say a subobject is decidable if its associated predicate is pointwise a decidable type. It turns out that these conditions are equivalent: a subobject is decidable if, and only if, it is complemented. Itβs immediate that decidable subobjects are complemented: given a decision procedure , the fibres and are disjoint and their union is all of .
is-decidable : β {β} {A : Type β} (p : β A) β Type _ is-decidable p = β a β Dec (a β p) is-decidableβis-complemented : (p : β A) β is-decidable p β is-complemented p is-decidableβis-complemented {A = A} p dec = inv , intersection , union where inv : β A inv x = el (Β¬ (x β p)) hlevel! intersection : (p β© inv) β minimal intersection x (xβp , xβp) = lift (xβp xβp) union : maximal β (p βͺ inv) union x wit with dec x ... | yes xβp = inc (inl xβp) ... | no xβp = inc (inr xβp)
For the converse, since decidability of a proposition is itself a proposition, it suffices to assume we have an inhabitant of . Assuming that , we must show that : But by the definition of complemented subobject, the intersection is empty.
is-complementedβis-decidable : (p : β A) β is-complemented p β is-decidable p is-complementedβis-decidable p (pβ»ΒΉ , intersection , union) elt = β‘-rec! (Ξ» { (inl xβp) β yes xβp ; (inr xβpβ»ΒΉ) β no Ξ» xβp β Lift.lower $ intersection elt (xβp , xβpβ»ΒΉ) }) (union elt tt)
Decidable subobject classifiersπ
In the same way that we have a (large) type of all propositions of size , the decidable (complemented) subobjects also have a classifying object: Any two-element type with decidable equality! This can be seen as a local instance of excluded middle: the complemented subobjects are precisely those satisfying , and so they are classified by the βclassical subobject classifierβ .
decidable-subobject-classifier : (A β Bool) β (Ξ£[ p β β A ] (is-decidable p)) decidable-subobject-classifier = eqv where
In much the same way that the subobject represented by a map is the fibre over , the subobject represented by a map is the fibre over . This is a decidable subobject because has decidable equality.
to : (A β Bool) β (Ξ£[ p β β A ] (is-decidable p)) to map .fst x = el (map x β‘ true) hlevel! to map .snd p = Bool-elim (Ξ» p β Dec (p β‘ true)) (yes refl) (no (Ξ» p β trueβ false (sym p))) (map p)
Conversely, to each decidable subobject and element we associate a boolean such that if and only if . Projecting the boolean and forgetting the equivalence gives us a map associated with , as desired; The characterisation of serves to smoothen the proof that this process is inverse to taking fibres over .
from : (pr : Ξ£[ p β β A ] (is-decidable p)) (x : A) β (Ξ£[ b β Bool ] ((b β‘ true) β (x β pr .fst))) from (p , dec) elt = Dec-elim (Ξ» _ β Ξ£ Bool (Ξ» b β (b β‘ true) β (elt β p))) (Ξ» y β true , prop-ext! (Ξ» _ β y) (Ξ» _ β refl)) (Ξ» xβp β false , prop-ext! (Ξ» p β absurd (trueβ false (sym p))) (Ξ» x β absurd (xβp x))) (dec elt) eqv = IsoβEquiv Ξ» where .fst β to .snd .is-iso.inv p x β from p x .fst .snd .is-iso.rinv pred β Ξ£-prop-path! $ β-ext (Ξ» x w β from pred x .snd .fst w) (Ξ» x p β Equiv.from (from pred x .snd) p) .snd .is-iso.linv pred β funext Ξ» x β Bool-elim (Ξ» p β from (to Ξ» _ β p) x .fst β‘ p) refl refl (pred x)
where is regarded as the top element of its own subobject latticeβ©οΈ