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.

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!

  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 =
  βˆ₯-βˆ₯-rec!  (Ξ» { (inl x∈p)   β†’ yes x∈p
             ; (inr x∈p⁻¹) β†’ no Ξ» x∈p β†’ intersection elt (x∈p , x∈p⁻¹)
    (union elt tt)

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”

  : {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!
  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β†©οΈŽ