{-# 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\subseteq p\cup (A\setminus p)$¹, and $(p\cap (A\setminus p))\subseteq \varnothing \text{.}$ Because of $\mathbb{P}(A)\text{’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\text{,}$ the fibres $p^{\ast }(\mathrm{yes}(x))$ and $p^{\ast }(\mathrm{no}(x))$ are disjoint and their union is all of $A\text{.}$

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 )

  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\in p)\coprod (x\in p^{-1})\text{.}$ Assuming that $x\in p^{-1}\text{,}$ we must show that $x\notin p\text{:}$ 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 =
  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 ${\mathrm{Prop}}_{\kappa }$ of all propositions of size $\kappa \text{,}$ 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\vee \neg P\text{,}$ and so they are classified by the “classical subobject classifier” $2:=\{0,1\}\text{.}$

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\to \mathrm{Prop}$ is the fibre over $\top \text{,}$ the subobject represented by a map $A\to 2$ is the fibre over $\mathtt{true}\text{.}$ 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\text{.}$ Projecting the boolean and forgetting the equivalence gives us a map $A\to 2$ associated with $p\text{,}$ as desired; The characterisation of $b$ serves to smoothen the proof that this process is inverse to taking fibres over $\mathtt{true}\text{.}$

  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.from 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)