{-# OPTIONS -vtactic.hlevel:10 #-}
open import 1Lab.Prelude

open import Data.Power
open import Data.Bool
open import Data.Dec
open import Data.Sum

module Data.Power.Complemented where


# Complemented subobjectsπ

A subobject $p : \mathbb{P}(A)$ of a type $A$ is called complemented if there is a subobject $A \setminus p$ such that $A \sube p \cup (A \setminus p)$1, and $(p \cap (A \setminus p)) \sube \emptyset$. Because of $\mathbb{P}(A)$βs lattice structure, these containments suffice to establish equality.

private variable
β : Level
A : Type β
p q r : β A

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^*(\mathrm{yes}(x))$ and $p^*(\mathrm{no}(x))$ are disjoint and their union is all of $A$.

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 $(x \in p) \coprod (x \in p^{-1})$. Assuming that $x \in p^{-1}$, we must show that $x \notin p$: But by the definition of complemented subobject, the intersection $(p \cap 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 =
β‘-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 $\mathrm{Prop}_\kappa$ of all propositions of size $\kappa$, 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 \lor \neg P$, and so they are classified by the βclassical subobject classifierβ $2 := \{ 0, 1 \}$. 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 $A \to \mathrm{Prop}$ is the fibre over $\top$, the subobject represented by a map $A \to 2$ is the fibre over $\mathtt{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! 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 : \mathbb{P}(A)$ and element $x : A$ we associate a boolean $b$ such that $(b \equiv \mathtt{true})$ if and only if $x \in p$. Projecting the boolean and forgetting the equivalence gives us a map $A \to 2$ associated with $p$, as desired; The characterisation of $b$ serves to smoothen the proof that this process is inverse to taking fibres over $\mathtt{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)


1. where $A$ is regarded as the top element of its own subobject latticeβ©οΈ