{-# 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 of a type is called complemented if there is a subobject such that 1, and Because of 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 the fibres and are disjoint and their union is all of

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 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 =
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 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 : 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 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 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 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)


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