open import Cat.Instances.StrictCat open import Cat.Instances.Discrete hiding (Disc) open import Cat.Instances.Functor open import Cat.Instances.Product open import Cat.Functor.Adjoint open import Cat.Univalent open import Cat.Prelude module Cat.Instances.StrictCat.Cohesive where

# Strict-cats is “cohesive”🔗

We prove that the category ${{{\mathfrak{Cat}}}_{\mathrm{strict}}}$ admits an adjoint quadruple

$\Pi_0 \dashv {\mathrm{Disc}} \dashv \Gamma \dashv {\mathrm{Codisc}}$

where the “central” adjoint $\Gamma$ 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 ${\mathrm{Sets}}$. The left- and right- adjoints to ${\mathrm{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 ${\mathrm{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.

**Note**: 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
$\Gamma$
sends each category to its set of points: see the last section. Strictly
speaking, the left adjoint to
$\Gamma$
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

For the adjunction unit, we’re asked to provide a natural transformation from the identity functor to $\Gamma \circ {\mathrm{Disc}}$; Since the object set of ${\mathrm{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
${\mathrm{Disc}}(\Gamma(X)) \to X$,
naturally in
$X$.
Since morphisms in discrete categories are paths, for a map
$x \equiv 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 : Precategory.Ob (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}

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
${{\mathbf{Sets}}}\to {{{\mathfrak{Cat}}}_{\mathrm{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 $\Gamma$. 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
$\Gamma$
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 \mapsto {\mathbf{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 ${\mathbf{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 ${\mathbf{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-id f)

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: Nat-path, funext, and Functor-path.

g : GlobalSections => Γ g .η x f = F₀ f (lift tt) g .is-natural x y f = refl f∘g : f ∘nt g ≡ idnt f∘g = Nat-path λ c → funext λ x → Functor-path (λ x → refl) λ f → sym (F-id x) g∘f : g ∘nt f ≡ idnt g∘f = Nat-path λ _ i x → x

# 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
$\mathcal{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 : \mathcal{C}$ are in the same connected component if there is a map $r : x \to 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) \to 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 $\mathcal{X} \to {\mathrm{Disc}}(\Pi_0(\mathcal{X}))$. We send $x$ to its connected component, and we must send a map $r : x \to 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 = record { F₀ = inc ; F₁ = quot ; F-id = squash _ _ _ _ ; F-∘ = λ _ _ → squash _ _ _ _ } adj .unit .is-natural x y f = Functor-path (λ x → refl) λ _ → squash _ _ _ _

The adjunction counit is an assignment of functions $\Pi_0({\mathrm{Disc}}(X)) \to 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 = funext (Coeq-elim-prop (λ _ → y .is-tr _ _) λ _ → refl)

The triangle identities are again straightforwardly checked.

adj .zig {x} = funext (Coeq-elim-prop (λ _ → squash _ _) λ x → refl) 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 $\pi_0$ of the product category onto $\pi_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!) (λ (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 (a , b) = Coeq-elim-prop₂ {C = λ x y → f (isom .inv (x , y)) ≡ (x , y)} (λ _ _ → ×-is-hlevel 2 squash squash _ _) (λ _ _ → refl) a b isom .linv = Coeq-elim-prop (λ _ → squash _ _) λ _ → refl

## Pieces have points🔗

An important property of the cohesive quadruple defined above is that
the canonically-defined natural morphism
$\Gamma(X) \to \Pi_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} y → ∥ fibre (Points→Pieces {ℓ} .η x) y ∥ pieces-have-points = Coeq-elim-prop (λ _ → squash) λ x → inc (x , refl)