open import 1Lab.Reflection.Copattern

open import Cat.Diagram.Pullback.Properties
open import Cat.Displayed.GenericObject
open import Cat.Instances.Sets.Complete
open import Cat.Diagram.Pullback.Along
open import Cat.Diagram.Limit.Finite
open import Cat.Displayed.Cartesian
open import Cat.Diagram.Pullback
open import Cat.Diagram.Terminal
open import Cat.Instances.Sets
open import Cat.Prelude hiding (Ω ; true)

import Cat.Displayed.Instances.Subobjects.Reasoning as Subr
import Cat.Displayed.Instances.Subobjects as Subobjs
import Cat.Reasoning

module Cat.Diagram.Omega where

Subobject classifiers🔗

In an arbitrary category $\mathcal{C}\text{,}$ a subobject of $X$ is, colloquially speaking, given by a monomorphism $m:A\hookrightarrow X\text{.}$ Formally, though, we must consider the object $A$ to be part of this data, since we can only speak of morphisms if we already know their domain and codomain. The generality in the definition means that the notion of subobject applies to completely arbitrary $\mathcal{C}\text{,}$ but in completely arbitrary situations, the notion might be very badly behaved.

There are several observations we can make about $\mathcal{C}$ that “tame” the behaviour of ${\mathrm{Sub}}_{\mathcal{C}}(X)\text{.}$ For example, if it has pullbacks, then $\mathrm{Sub}(-)$ is a fibration, so that there is a universal way of re-indexing a subobject $x:\mathrm{Sub}(X)$ along a morphism $f:Y\to X\text{,}$ and if it has images, it’s even a bifibration, so that each of these reindexings has a left adjoint, giving an interpretation of existential quantifiers. If $\mathcal{C}$ is a regular category, existential quantifiers and substitution commute, restricting the behaviour of subobjects even further.

However, there is one assumption we can make about $\mathcal{C}$ that rules them all: it has a generic subobject, so that $\mathrm{Sub}(X)$ is equivalent to a given $\mathbf{Hom}\text{-set}$ in $\mathcal{C}\text{.}$ A generic subobject is a morphism $\top :\Omega \ast \to \Omega$ so that, for any a subobject $m:A\hookrightarrow X\text{,}$ there is a unique arrow $┌m┐$ making the square

into a pullback. We can investigate this definition by instantiating it in $\mathbf{Sets}\text{,}$ which does have a generic subobject. Given an embedding $m:A\hookrightarrow X\text{,}$ we have a family of propositions $┌m┐:X\to \Omega$ which maps $x:X$ to $m^{\ast }(x)\text{,}$ the fibre of $m$ over $x\text{.}$ The square above also computes a fibre, this time of $┌m┐\text{,}$ and saying that it is $m$ means that $┌m┐$ assigns $\top$ to precisely those $x:X$ which are in $m\text{.}$

module _ {o ℓ} (C : Precategory o ℓ) where
  open Cat.Reasoning C
  open Subobjs C

  record is-generic-subobject {Ω} (true : Subobject Ω) : Type (o ⊔ ℓ) where
    field
      name : ∀ {X} (m : Subobject X) → Hom X Ω
      classifies
        : ∀ {X} (m : Subobject X)
        → is-pullback-along C (m .map) (name m) (true .map)
      unique
        : ∀ {X} {m : Subobject X} {nm : Hom X Ω}
        → is-pullback-along C (m .map) nm (true .map)
        → nm ≡ name m

  record Subobject-classifier : Type (o ⊔ ℓ) where
    field
      {Ω}     : Ob
      true    : Subobject Ω
      generic : is-generic-subobject true
    open is-generic-subobject generic public

While the definition of is-generic-subobject can be stated without assuming that $\mathcal{C}$ has any limits at all, we’ll need to assume that $\mathcal{C}$ has pullbacks to get anything of value done. Before we get started, however, we’ll prove a helper theorem that serves as a “smart constructor” for Subobject-classifier, simplifying the verification of the universal property in case $\mathcal{C}$ is univalent and has all finite limits (in particular, a terminal object).

module _ {o ℓ} {C : Precategory o ℓ} (fc : Finitely-complete C) (cat : is-category C) where
  open Subobject-classifier
  open is-generic-subobject
  open Cat.Reasoning C
  open Subr (fc .Finitely-complete.pullbacks)
  open Terminal (fc .Finitely-complete.terminal) using (top)

  point→subobject : ∀ {A} (it : Hom top A) → Subobject A
  point→subobject it .domain = top
  point→subobject it .map = it
  point→subobject it .monic g h x = Terminal.!-unique₂ (fc .Finitely-complete.terminal) _ _

Assuming that we have a terminal object, we no longer need to specify the arrow $\mathtt{true}$ as an arbitrary element of $\mathrm{Sub}(\Omega )$ — we can instead ask for a point $\mathtt{true}:\top \to \Omega$ instead. Since we have pullbacks, we also have the change-of-base operation $f^{\ast }(-):\mathrm{Sub}(B)\to \mathrm{Sub}(A)$ for any $f:A\to B\text{,}$ which allows us to simplify the condition that “$m$ is the pullback of $n$ along $f$”, which requires constructing a pullback square, to the simpler $m\cong f^{\ast }n\text{.}$ The theorem is that it suffices to ask for:

• The point $\mathtt{true}:\top \to \Omega$ corresponding to the generic subobject,
• An operation $┌-┐:\mathrm{Sub}(A)\to \mathbf{Hom}(A,\Omega )$ which maps subobjects to their names,
• A witness that, for any $m:\mathrm{Sub}(A)\text{,}$ we have $m\cong ┌m{┐}^{\ast }\mathtt{true}\text{,}$ and
• A witness that, for any $h:\mathbf{Hom}(A,\Omega )\text{,}$ we have $h=┌h^{\ast }\mathtt{true}┐\text{.}$

These two conditions amount to saying that $┌-┐$ and $(-{)}^{\ast }\top$ form an equivalence between the sets $\mathrm{Sub}(A)$ and $\mathbf{Hom}(A,\Omega )\text{,}$ for all $A\text{.}$ Note that we do not need to assume naturality for $┌-┐$ since it is an inverse equivalence to $(-{)}^{\ast }\mathtt{true}\text{,}$ which is already natural.

  from-classification
    : ∀ {Ω} (true : Hom top Ω)
    → (name : ∀ {A} (m : Subobject A) → Hom A Ω)
    → (∀ {A} (m : Subobject A) → m ≅ₘ name m ^* point→subobject true)
    → (∀ {A} (h : Hom A Ω) → name (h ^* point→subobject true) ≡ h)
    → Subobject-classifier C
  from-classification tru nm invl invr = done where
    done : Subobject-classifier C
    done .Ω = _
    done .true = point→subobject tru
    done .generic .name = nm
    done .generic .classifies m = iso→is-pullback-along {m = m} {n = point→subobject tru} (invl m)

Note that the uniqueness part of the universal property is satisfied by the last constraint on $┌-┐\text{:}$ the is-pullback-along assumption amounts to saying that $m\equiv h^{\prime \ast }\mathtt{true}\text{,}$ by univalence of $\mathrm{Sub}(A)\text{;}$ so we have $$┌m┐=┌h^{\prime \ast }\mathtt{true}┐=h^{\prime }\text{.}$$

    done .generic .unique {m = m} {h'} p =
      let
        rem₁ : m ≡ h' ^* point→subobject tru
        rem₁ = Sub-is-category cat .to-path $
          is-pullback-along→iso {m = m} {n = point→subobject tru} p
      in sym (ap nm rem₁ ∙ invr _)

  record make-subobject-classifier : Type (o ⊔ ℓ) where
    field
      {Ω}  : Ob
      true : Hom top Ω
      name : ∀ {A} (m : Subobject A) → Hom A Ω
      named-name : ∀ {A} (m : Subobject A) → m ≅ₘ name m ^* point→subobject true
      name-named : ∀ {A} (h : Hom A Ω) → name (h ^* point→subobject true) ≡ h

module _ where
  open make-subobject-classifier hiding (Ω)

  to-subobject-classifier : ∀ {o ℓ} {C : Precategory o ℓ} (fc : Finitely-complete C) (cat : is-category C) → make-subobject-classifier fc cat → Subobject-classifier C
  to-subobject-classifier fc cat mk = from-classification fc cat (mk .true) (mk .name) (mk .named-name) (mk .name-named)

Sets-subobject-classifier : ∀ {ℓ} → Subobject-classifier (Sets ℓ)
Sets-subobject-classifier {ℓ} =
  to-subobject-classifier Sets-finitely-complete Sets-is-category mk where
  open Subr (Sets-pullbacks {ℓ})
  open Cat.Prelude using (Ω)
  open make-subobject-classifier hiding (Ω)

The prototypical category with a subobject classifier is the category of sets. Since it is finitely complete and univalent, our helper above will let us swiftly dispatch the construction. Our subobject classifier is given by the type of propositions, $\Omega \text{,}$ lifted to the right universe. The name of a subobject $m:\mathrm{Sub}(A)$ is the family of propositions $x\mapsto m^{\ast }(x)\text{.}$ Note that we must squash this fibre down so it fits in $\Omega \text{,}$ but this squashing is benign because $m$ is a monomorphism (hence, an embedding).

  unbox : ∀ {A : Set ℓ} (m : Subobject A) {x} → □ (fibre (m .map) x) → fibre (m .map) x
  unbox m = □-out (monic→is-embedding (hlevel ) (λ {C} g h p → m .monic {C} g h p) _)

  mk : make-subobject-classifier _ _
  mk .make-subobject-classifier.Ω = el! (Lift _ Ω)
  mk .true _ = lift ⊤Ω
  mk .name m x = lift (elΩ (fibre (m .map) x))

Showing that this name function actually works takes a bit of fiddling, but it’s nothing outrageous.

  mk .named-name m = Sub-antisym
    record
      { map = λ w → m .map w , lift tt , ap lift (to-is-true (inc (w , refl)))
      ; sq  = refl
      }
    record { sq = ext λ x _ p → sym (unbox m (from-is-true p) .snd )}
  mk .name-named h = ext λ a → Ω-ua
    (rec! λ x _ p y=a → from-is-true (ap h (sym y=a) ∙ p))
    (λ ha → inc ((a , lift tt , ap lift (to-is-true ha)) , refl))

As generic objects🔗

We can connect the definition above with that of generic objects in a fibration: specifically, a generic subobject is a generic object in the fibration of subobjects. The similar naming is not an accident: the proof boils down to shuffling data around.

module _ {o ℓ} (C : Precategory o ℓ)  where
  open is-generic-subobject
  open is-pullback-along
  open Generic-object
  open Cat.Reasoning C using (pulll)
  open is-cartesian
  open Subobjs C

  from-generic-subobject
    : ∀ {Ω} {tru : Subobject Ω} → is-generic-subobject C tru
    → Generic-object Subobjects tru
  from-generic-subobject gen .classify    = gen .name
  from-generic-subobject gen .classify' s = record { sq = gen .classifies s .square }
  from-generic-subobject gen .classify-cartesian s = record
    { universal = λ {u} {u'} m a → record
      { map = gen .classifies s .universal (pulll refl ∙ a .sq)
      ; sq = sym (gen .classifies s .p₁∘universal)
      }
    ; commutes  = λ m h → prop!
    ; unique    = λ m h → prop!
    }

open Subobject-classifier using (unique)

module props {o ℓ} {C : Precategory o ℓ} (pb : has-pullbacks C) (so : Subobject-classifier C) where
  open Subobject-classifier so renaming (Ω to Ω')
  open is-pullback-along
  open Cat.Reasoning C
  open is-invertible
  open is-pullback
  open Pullback
  open Subr pb

  named : ∀ {A} (f : Hom A Ω') → Subobject A
  named f = f ^* true

  named-name : ∀ {A} {m : Subobject A} → m ≅ₘ named (name m)
  named-name = is-pullback-along→iso (classifies _)

  name-injective : ∀ {A} {m n : Subobject A} → name m ≡ name n → m ≅ₘ n
  name-injective {m = m} {n} p =
    m              Sub.≅⟨ named-name ⟩Sub.≅
    named (name m) Sub.≅⟨ path→iso (ap named p) ⟩Sub.≅
    named (name n) Sub.≅˘⟨ named-name ⟩Sub.≅˘
    n              Sub.≅∎

  name-ap : ∀ {A} {m n : Subobject A} → m ≅ₘ n → name m ≡ name n
  name-ap {m = m} im = so .unique record
    { top       = classifies m .top ∘ im .Sub.from .map
    ; has-is-pb = subst-is-pullback (sym (im .Sub.from .sq) ∙ eliml refl) refl refl refl
        (is-pullback-iso (≅ₘ→iso im) (classifies m .has-is-pb))
    }

  is-total : ∀ {A} (f : Hom A Ω') → Type _
  is-total f = is-invertible (pb f (true .map) .p₁)

  factors→is-total : ∀ {A} {f : Hom A Ω'} → Factors f (true .map) → is-total f
  factors→is-total (h , p) .inv = pb _ _ .universal (idr _ ∙ p)
  factors→is-total (h , p) .inverses = record
    { invl = pb _ _ .p₁∘universal
    ; invr = Pullback.unique₂ (pb _ _) {p = pushl p}
      (pulll (pb _ _ .p₁∘universal) ∙ idl _)
      (pulll (pb _ _ .p₂∘universal))
      (idr _)
      (idr _ ∙ true .monic _ _ (sym (pulll (sym p) ∙ pb _ (true .map) .square)))
    }

  is-total→factors : ∀ {A} {f : Hom A Ω'} → is-total f → Factors f (true .map)
  is-total→factors {f = f} inv = record { snd = done } where
    rem₁ : is-pullback-along C id f (true .map)
    rem₁ = record { has-is-pb = record
      { square       = idr _ ∙ sym (pulll (sym (pb _ _ .square)) ∙ cancelr (inv .is-invertible.invl))
      ; universal    = λ {P'} {p₁'} _ → p₁'
      ; p₁∘universal = idl _
      ; p₂∘universal = λ {P'} {p₁'} {p₂'} {α} → true .monic _ _ $
          pulll (pulll (sym (pb _ _ .square)) ∙ cancelr (inv .is-invertible.invl))
        ∙ α
      ; unique       = λ p _ → introl refl ∙ p
      }}

    done =
      f                              ≡⟨ so .unique rem₁ ⟩≡
      name ⊤ₘ                        ≡⟨ intror refl ⟩≡
      name ⊤ₘ ∘ id                   ≡⟨ classifies ⊤ₘ .square ⟩≡
      true .map ∘ classifies ⊤ₘ .top ∎

  true-domain-is-terminal : is-terminal C (true .domain)
  true-domain-is-terminal X .centre  = classifies ⊤ₘ .top
  true-domain-is-terminal X .paths h = true .monic _ _ (sym (is-total→factors record
    { inv      = pb _ _ .universal (pullr refl)
    ; inverses = record
      { invl = pb _ _ .p₁∘universal
      ; invr = Pullback.unique₂ (pb _ _) {p = pullr refl}
        (pulll (pb _ _ .p₁∘universal)) (extendl (pb _ _ .p₂∘universal)) id-comm
        (true .monic _ _ (extendl (sym (pb _ _ .square)) ∙ pullr (ap (h ∘_) id-comm)))
      }
    } .snd))