{-# 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:P(A)p : {\mathbb{P}}(A) of a type AA is called complemented if there is a subobject Aβˆ–pA \setminus p such that AβŠ†pβˆͺ(Aβˆ–p)A \sube p \cup (A \setminus p)1, and (p∩(Aβˆ–p))βŠ†βˆ…(p \cap (A \setminus p)) \sube \emptyset. Because of P(A){\mathbb{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 pp, the fibres pβˆ—(yes(x))p^*({\mathrm{yes}}(x)) and pβˆ—(no(x))p^*({\mathrm{no}}(x)) are disjoint and their union is all of AA.

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∈p)∐(x∈pβˆ’1)(x \in p) \coprod (x \in p^{-1}). Assuming that x∈pβˆ’1x \in p^{-1}, we must show that xβˆ‰px \notin p: But by the definition of complemented subobject, the intersection (p∩pβˆ’1)(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 PropΞΊ{\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∨¬PP \lor \neg P, and so they are classified by the β€œclassical subobject classifier” 2:={0,1}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β†’PropA \to {\mathrm{Prop}} is the fibre over ⊀\top, the subobject represented by a map Aβ†’2A \to 2 is the fibre over true\mathtt{true}. This is a decidable subobject because 22 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:P(A)p : {\mathbb{P}}(A) and element x:Ax : A we associate a boolean bb such that (b≑true)(b \equiv \mathtt{true}) if and only if x∈px \in p. Projecting the boolean and forgetting the equivalence gives us a map Aβ†’2A \to 2 associated with pp, as desired; The characterisation of bb serves to smoothen the proof that this process is inverse to taking fibres over true\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 AA is regarded as the top element of its own subobject latticeβ†©οΈŽ