module Cat.Instances.StrictCat.Cohesive where

# Strict-cats is “cohesive”🔗

We prove that the category $Cat_{strict}$ admits an adjoint quadruple

$Π_{0}⊣Disc⊣Γ⊣Codisc$where the “central” adjoint $Γ$ is the functor which sends a strict category to its underlying set of objects. This lets us treat categories as giving a kind of “spatial” structure over $Sets.$ The left- and right- adjoints to $Ob$ equip sets with the “discrete” and “codiscrete” spatial structures, where nothing is stuck together, or everything is stuck together.

The extra right adjoint to $Ob$ assigns a category to its set of connected components, which can be thought of as the “pieces” of the category. Two objects land in the same connected component if there is a path of morphisms connecting them, hence the name.

Generally, the term “cohesive” is applied to Grothendieck topoi,
which `Strict-cats`

is *very
far* from being. We’re using it here by analogy: There’s an adjoint
quadruple, where the functor
$Γ$
sends each category to its set of points: see the last section. Strictly
speaking, the left
adjoint to
$Γ$
isn’t defined by tensoring with `Sets`

,
but it *does* have the effect of sending
$S$
to the coproduct of
$S-many$
copies of the point category.

# Disc ⊣ Γ🔗

We begin by defining the object set functor.

Γ : Functor (Strict-cats o h) (Sets o) Γ .F₀ (C , obset) = el (Ob C) obset Γ .F₁ = F₀ Γ .F-id = refl Γ .F-∘ _ _ = refl

We must then prove that the assignment `Disc'`

extends to a functor from
`Sets`

, and prove that it’s left
adjoint to the functor `Γ`

we defined above. Then we
define the adjunction `Disc⊣Γ`

.

Disc : Functor (Sets ℓ) (Strict-cats ℓ ℓ) Disc .F₀ S = Disc' S , S .is-tr Disc .F₁ = lift-disc Disc .F-id = Functor-path (λ x → refl) λ f → refl Disc .F-∘ _ _ = Functor-path (λ x → refl) λ f → refl Disc⊣Γ : Disc {ℓ} ⊣ Γ Disc⊣Γ = adj where

abstract lemma : ∀ {A : Strict-cats ℓ ℓ .Precategory.Ob} {x y z : A .fst .Precategory.Ob} (f : y ≡ z) (g : x ≡ y) → subst (A .fst .Precategory.Hom _) (g ∙ f) (A .fst .Precategory.id) ≡ A .fst .Precategory._∘_ (subst (A .fst .Precategory.Hom _) f (A .fst .Precategory.id)) (subst (A .fst .Precategory.Hom _) g (A .fst .Precategory.id)) lemma {A = A} {x = x} = J' (λ y z f → (g : x ≡ y) → subst (X.Hom _) (g ∙ f) X.id ≡ subst (X.Hom _) f X.id X.∘ subst (X.Hom _) g X.id) λ x g → (subst-∙ (X.Hom _) g refl _ ·· transport-refl _ ·· sym (X.idl _)) ∙ ap₂ X._∘_ (sym (transport-refl _)) refl where module X = Precategory (A .fst)

For the adjunction `unit`

, we’re asked
to provide a natural transformation from the identity functor to
$Γ∘Disc;$
Since the object set of
$Disc(X)$
is simply
$X,$
the identity map suffices:

adj : Disc {ℓ} ⊣ Γ adj .unit = NT (λ _ x → x) λ x y f i o → f o

The adjunction counit is slightly more complicated, as we have to
give a functor
$Disc(Γ(X))→X,$
naturally in
$X.$
Since morphisms in discrete categories are paths, for a map
$x≡y$
(in `{- 1 -}`

), it
suffices to assume
$y$
really is
$x,$
and so the identity map suffices.

adj .counit = NT (λ x → F x) nat where F : (x : ⌞ Strict-cats ℓ ℓ ⌟) → Functor (Disc' (el _ (x .snd))) _ F X .F₀ x = x F X .F₁ p = subst (X .fst .Hom _) p (X .fst .id) {- 1 -} F X .F-id = transport-refl _ F X .F-∘ = lemma {A = X}

abstract nat : (x y : ⌞ Strict-cats ℓ ℓ ⌟) (f : Strict-cats ℓ ℓ .Precategory.Hom x y) → (F y F∘ (Disc F∘ Γ) .F₁ f) ≡ (f F∘ F x) nat x y f = Functor-path (λ x → refl) (J' (λ x y p → subst (Y.Hom _) (ap (f .F₀) p) Y.id ≡ f .F₁ (subst (X.Hom _) p X.id)) λ _ → transport-refl _ ·· sym (f .F-id) ·· ap (f .F₁) (sym (transport-refl _))) where module X = Precategory (x .fst) module Y = Precategory (y .fst)

Fortunately the triangle identities are straightforwardly checked.

adj .zig {x} = Functor-path (λ x i → x) λ f → x .is-tr _ _ _ _ adj .zag = refl

# Γ ⊣ Codisc🔗

The *codiscrete* category on a set
$X$
is the strict
category with object space
$X,$
and *all* hom-spaces contractible. The assignment of codiscrete
categories extends to a functor
$Sets→Cat_{strict},$
where we lift functions to act on object parts and the action on
morphisms is trivial.

Codisc : Functor (Sets ℓ) (Strict-cats ℓ ℓ) Codisc .F₀ S = Codisc' ∣ S ∣ , S .is-tr Codisc .F₁ f .F₀ = f Codisc .F₁ f .F₁ = λ _ → lift tt Codisc .F₁ f .F-id = refl Codisc .F₁ f .F-∘ = λ _ _ → refl Codisc .F-id = Functor-path (λ x → refl) λ f → refl Codisc .F-∘ _ _ = Functor-path (λ x → refl) λ f → refl

The codiscrete category functor is right adjoint to the object set functor $Γ.$ The construction of the adjunction is now simple in both directions:

Γ⊣Codisc : Γ ⊣ Codisc {ℓ} Γ⊣Codisc = adj where adj : _ ⊣ _ adj .unit = NT (λ x → record { F₀ = λ x → x ; F₁ = λ _ → lift tt ; F-id = refl ; F-∘ = λ _ _ → refl }) λ x y f → Functor-path (λ _ → refl) λ _ → refl adj .counit = NT (λ _ x → x) λ x y f i o → f o adj .zig = refl adj .zag = Functor-path (λ _ → refl) λ _ → refl

## Object set vs global sections🔗

Above, we defined the functor
$Γ$
by directly projecting the underlying set of each category. Normally in
the definition of a cohesion structure, we use the *global
sections* functor which maps
$x↦Hom(∗,x)$
(where
$∗$
is the terminal
object). Here we prove that these functors are naturally isomorphic,
so our abbreviation above is harmless.

Below, we represent the terminal category $∗$ as the codiscrete category on the terminal set. Using the codiscrete category here is equivalent to using the discrete category, but it is more convenient since the $Hom-sets$ are definitionally contractible.

module _ {ℓ} where import Cat.Morphism Cat[ Strict-cats ℓ ℓ , Sets ℓ ] as Nt GlobalSections : Functor (Strict-cats ℓ ℓ) (Sets ℓ) GlobalSections .F₀ C = el (Functor (Codisc' (Lift _ ⊤)) (C .fst)) (Functor-is-set (C .snd)) GlobalSections .F₁ G F = G F∘ F GlobalSections .F-id = funext λ _ → Functor-path (λ _ → refl) λ _ → refl GlobalSections .F-∘ f g = funext λ _ → Functor-path (λ _ → refl) λ _ → refl

Since `GlobalSections`

is a section of
the
$Hom$
functor, it acts on maps by composition. The functor identities hold
definitionally.

GlobalSections≅Γ : Γ {ℓ} Nt.≅ GlobalSections GlobalSections≅Γ = Nt.make-iso f g f∘g g∘f where open Precategory

We define a natural isomorphism from `Γ`

to the `GlobalSections`

functor by
sending each object to the constant functor on that object. This
assignment is natural because it is essentially independent of the
coordinate.

f : Γ => GlobalSections f .η x ob = record { F₀ = λ _ → ob ; F₁ = λ _ → x .fst .id ; F-id = refl ; F-∘ = λ _ _ → sym (x .fst .idl _) } f .is-natural x y f = funext λ _ → Functor-path (λ _ → refl) λ _ → sym (f .F-id)

In the opposite direction, the natural transformation is defined by
evaluating at the point. These natural transformations compose to the
identity almost definitionally, but Agda does need some convincing,
using our path helpers, `Functor-path`

and `trivial!`

.

g : GlobalSections => Γ g .η x f = f # lift tt g .is-natural x y f = refl f∘g : f ∘nt g ≡ idnt f∘g = ext λ c x → Functor-path (λ x → refl) λ f → sym (x .F-id) g∘f : g ∘nt f ≡ idnt g∘f = trivial!

# Connected components🔗

The set of connected components of a category is the quotient of the
object set by the “relation” generated by the `Hom`

sets. This is
not a relation because `Hom`

takes values in
sets, not propositions; Thus the quotient forgets precisely *how*
objects are connected. This is intentional!

π₀ : Precategory o h → Set (o ⊔ h) π₀ C = el (Ob C / Hom C) squash

The `π₀`

construction extends to a
functor `Π₀`

(capital pi for
**P**ieces) from `Strict-cats`

back to `Sets`

. We send a functor
$F$
to its object part, but postcomposing with the map `inc`

which sends an
object of
$D$
to the connected component it inhabits.

Π₀ : Functor (Strict-cats o h) (Sets (o ⊔ h)) Π₀ .F₀ (C , _) = π₀ C Π₀ .F₁ F = Quot-elim (λ _ → squash) (λ x → inc (F .F₀ x)) λ x y r → glue (_ , _ , F .F₁ r)

We must prove that this assignment respects the quotient, which is where the morphism part of the functor comes in: Two objects $x,y:C$ are in the same connected component if there is a map $r:x→y;$ To show that $F_{0}(x)$ and $F_{0}(y)$ are also in the same connected component, we must give a map $F_{0}(x)→F_{0}(y),$ but this can be canonically chosen to be $F_{1}(r).$

Π₀ .F-id = funext (Coeq-elim-prop (λ _ → squash _ _) λ x → refl) Π₀ .F-∘ f g = funext (Coeq-elim-prop (λ _ → squash _ _) λ x → refl)

The adjunction `unit`

is a natural
assignment of functors
$X→Disc(Π_{0}(X)).$
We send
$x$
to its connected component, and we must send a map
$r:x→y$
to an equality between the connected components of
$x$
and
$y;$
But we get this from the quotient.

Π₀⊣Disc : Π₀ ⊣ Disc {ℓ} Π₀⊣Disc = adj where adj : _ ⊣ _ adj .unit .η x = Disc-into _ inc quot adj .unit .is-natural x y f = Functor-path (λ x → refl) λ _ → squash _ _ _ _

The adjunction `counit`

is an
assignment of functions
$Π_{0}(Disc(X))→X.$
This is essentially a natural isomorphism: the set of connected
components of a discrete category is the same set we started with.

adj .counit .η X = Quot-elim (λ _ → X .is-tr) (λ x → x) λ x y r → r adj .counit .is-natural x y f = trivial!

The triangle identities are again straightforwardly checked.

adj .zig {x} = trivial! adj .zag = Functor-path (λ x → refl) λ f → refl

Furthermore, we can prove that the connected components of a product category are product sets of connected components.

Π₀-preserve-prods : ∀ {C D : Precategory o h} → π₀ ʻ (C ×ᶜ D) ≡ (π₀ ʻ C × π₀ ʻ D) Π₀-preserve-prods {C = C} {D = D} = Iso→Path (f , isom) where open is-iso

We have a map splitting $π_{0}$ of the product category onto $π_{0}$ of each factor. This maps respect the quotient because we can also split the morphisms.

f : π₀ ʻ (C ×ᶜ D) → π₀ ʻ C × π₀ ʻ D f = Quot-elim (λ _ → hlevel 2) (λ (a , b) → inc a , inc b) λ (x , x') (y , y') (f , g) i → glue (x , y , f) i , glue (x' , y' , g) i

This map has an inverse given by joining up the pairs:

isom : is-iso f isom .inv (a , b) = Coeq-rec₂ squash (λ x y → inc (x , y)) (λ a (x , y , r) i → glue ((x , a) , (y , a) , r , Precategory.id D) i) (λ a (x , y , r) i → glue ((a , x) , (a , y) , Precategory.id C , r) i) a b isom .rinv = elim! λ x y → refl isom .linv = elim! λ x y → refl

## Pieces have points🔗

An important property of the cohesive quadruple defined above is that
the canonically-defined natural morphism
$Γ(X)→Π_{0}(X)$
is surjective, i.e. *each piece has at least one point*.

Points→Pieces : Γ {ℓ} {ℓ} => Π₀ Points→Pieces .η _ x = inc x Points→Pieces .is-natural x y f i o = inc (f .F₀ o) pieces-have-points : ∀ {x} → is-surjective (Points→Pieces {ℓ} .η x) pieces-have-points = elim! λ x → inc (x , refl)