module Data.Power.Complemented where

# Complemented subobjectsπ

A subobject
$p:P(A)$
of a type
$A$
is called **complemented** if there is a subobject
$Aβp$
such that
$Aβpβͺ(Aβp)$^{1}, and
$(pβ©(Aβp))ββ.$
Because of
$P(A)β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
$p,$
the fibres
$p_{β}(yes(x))$
and
$p_{β}(no(x))$
are disjoint and their union is all of
$A.$

is-decidable : β {β} {A : Type β} (p : β A) β Type _ is-decidable {A = A} p = (a : 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 1) intersection : (p β© inv) β minimal intersection x (xβp , xβp) = 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
$(xβp)β(xβp_{β1}).$
Assuming that
$xβp_{β1},$
we must show that
$xβ/p:$
But by the definition of complemented subobject, the intersection
$(pβ©p_{β1})$
is empty.

is-complementedβis-decidable : (p : β A) β is-complemented p β is-decidable p is-complementedβis-decidable p (pβ»ΒΉ , intersection , union) elt = case union elt tt of Ξ» where (inl xβp) β yes xβp (inr xβΒ¬p) β no Ξ» xβp β intersection elt (xβp , xβΒ¬p)

# Decidable subobject classifiersπ

In the same way that we have a (large) type $Prop_{ΞΊ}$ 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 $Pβ¨Β¬P,$ and so they are classified by the βclassical subobject classifierβ $2:={0,1}.$

decidable-subobject-classifier : {A : Type β} β (A β Bool) β (Ξ£[ p β β A ] (is-decidable p)) decidable-subobject-classifier {A = A} = eqv where

In much the same way that the subobject represented by a map $AβProp$ is the fibre over $β€,$ the subobject represented by a map $Aβ2$ is the fibre over $true.$ This is a decidable subobject because $2$ has decidable equality.

to : (A β Bool) β (Ξ£[ p β β A ] (is-decidable p)) to map .fst x = el (map x β‘ true) (hlevel 1) 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 $p:P(A)$ and element $x:A$ we associate a boolean $b$ such that $(bβ‘true)$ if and only if $xβp.$ Projecting the boolean and forgetting the equivalence gives us a map $Aβ2$ associated with $p,$ as desired; The characterisation of $b$ serves to smoothen the proof that this process is inverse to taking fibres over $true.$

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 $A$ is regarded as the top element of its own subobject latticeβ©οΈ