open import Cat.Diagram.Pullback.Along
open import Cat.Instances.FinSets
open import Cat.Diagram.Pullback
open import Cat.Diagram.Omega
open import Cat.Prelude

open import Data.Fin.Finite
open import Data.Fin.Base

import Cat.Displayed.Instances.Subobjects as Sub

open is-generic-subobject
open is-pullback-along
open Sub FinSets
open Subobject

module Cat.Instances.FinSets.Omega where

The subobject classifier in FinSets🔗

In the category of finite sets, the set $\{0,1\}\text{,}$ with the inclusion of $1\text{,}$ is a generic subobject. The construction of the name of a subobject $S\hookrightarrow X$ is by cases: since finite sets are closed under dependent sum and identity, they are closed under fibres, so we can define the name function at $x:X$ by cases on the cardinality of $m^{\ast }(x)\text{.}$

fin-name : ∀ {X} → Subobject X → Fin X → Fin 
fin-name {X = X} so m with cardinality {T = fibre (so .map) m}
... | zero  = 
... | suc x = 

tru : Subobject 
tru .domain = 
tru .map _ = 
tru .monic g h x = ext λ e → Fin-cases {P = λ x → x ≡ h e} (Fin-cases {P = λ x →  ≡ x} refl (λ ()) (h e)) (λ ()) (g e)

private
  inj : ∀ {X} (m : Subobject X) → injective (m .map)
  inj m {a} {b} α = m .monic {c = } (λ _ → a) (λ _ → b) (ext λ _ → α) $ₚ 

This construction satisfies the evident ‘universal property’: its value at $x$ is $1$ if, and only if, the fibre $m^{\ast }(x)$ is actually inhabited (in which case it’s even contractible, since subobjects of finite sets are embeddings).

from-name : ∀ {X} (m : Subobject X) x → fin-name m x ≡  → fibre (m .map) x
from-name m x p with cardinality {T = fibre (m .map) x} | enumeration {T = fibre (m .map) x}
... | zero  | e = absurd (fzero≠fsuc p)
... | suc x | e = ∥-∥-out (injective→is-embedding! (inj m) _) (case e of λ eqv → pure (Equiv.from eqv ))

to-name : ∀ {X} (m : Subobject X) x → fibre (m .map) x → fin-name m x ≡ 
to-name m x p with cardinality {T = fibre (m .map) x} | enumeration {T = fibre (m .map) x}
... | zero  | e = absurd (case e of λ eqv → Fin-absurd (Equiv.to eqv p))
... | suc x | e = refl

These two helpers show that $m$ is the pullback of the true arrow along $┌m┐\text{,}$ as required.

FinSets-omega : Subobject-classifier FinSets
FinSets-omega .Subobject-classifier.Ω = 
FinSets-omega .Subobject-classifier.true = tru
FinSets-omega .Subobject-classifier.generic .name       = fin-name
FinSets-omega .Subobject-classifier.generic .classifies m = record { top = λ _ →  ; has-is-pb = fb } where
  fb : is-pullback FinSets (m .map) (fin-name m) (λ _ → ) (λ _ → )
  fb .is-pullback.square        = ext λ a → to-name m _ (a , refl)
  fb .is-pullback.universal α x = from-name m _ (happly α x) .fst
  fb .is-pullback.p₁∘universal  = ext λ a → from-name m _ _ .snd
  fb .is-pullback.p₂∘universal {p₂' = p₂'}  = ext λ a → Fin-cases {P = λ x →  ≡ x} refl (λ ()) (p₂' a)
  fb .is-pullback.unique a e = ext λ x → inj m (happly a x ∙ sym (from-name m _ _ .snd))

We can show uniqueness also by cases on the cardinality of each fibre. First, if the fibre is inhabited, then let $x^{\prime }$ be the preimage of $x\text{;}$ we then have $n(x)=n(m{x}^{\prime })=1$ as needed.

FinSets-omega .Subobject-classifier.generic .unique {m = m} {nm} pb = ext uniq where
  uniq : ∀ x → nm x ≡ fin-name m x
  uniq x with cardinality {T = fibre (m .map) x} | enumeration {T = fibre (m .map) x} | from-name m x
  ... | suc n | e | f with (x' , α) ← f refl = ap nm (sym α) ∙ happly (pb .square) _

If the fibre is uninhabited, we show that $n(x)=0$ by showing it can not be $1\text{.}$ For if it were $1\text{,}$ its universal property as a pullback would let us get our hands on an element of $m^{\ast }(x)$ — but we already know that this type has cardinality zero.

  ... | zero | e | _ =
    let
      a : nm x ≡ fin  → ⊥
      a w =
        let
          vl = pb .universal {P' = } {p₁' = λ _ → x} {p₂' = λ _ → } (ext λ _ → w) 
          it : fibre (m .map) x
          it = vl , pb .p₁∘universal · 
        in case e of λ eqv → absurd (Fin-absurd (Equiv.to eqv it))
    in
      Fin-cases {P = λ e → nm x ≡ e → nm x ≡ } (λ x → x)
        (fin-cons (λ nmx=0 → absurd (a nmx=0)) λ ())
        (nm x) refl