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.Prelude

module Cat.Instances.StrictCat.Cohesive where

private variable
  ℓ o h : Level

open Precategory
open Functor
open _=>_
open _⊣_

Strict-cats is “cohesive”🔗

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

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}\text{.}$ 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.

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 $\Gamma \circ \mathrm{Disc}\text{;}$ Since the object set of $\mathrm{Disc}(X)$ is simply $X\text{,}$ 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\text{,}$ naturally in $X\text{.}$ Since morphisms in discrete categories are paths, for a map $x\equiv y$ (in {- 1 -}), it suffices to assume $y$ really is $x\text{,}$ 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\text{,}$ and all hom-spaces contractible. The assignment of codiscrete categories extends to a functor $\mathbf{Sets}\to {\mathfrak{Cat}}_{\mathrm{strict}}\text{,}$ 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 \text{.}$ 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}(\ast ,x)$ (where $\ast$ 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 $\ast$ 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}\text{-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 .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 Pieces) 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\text{;}$ 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)\text{,}$ but this can be canonically chosen to be $F_1(r)\text{.}$

Π₀ .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}))\text{.}$ 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\text{;}$ 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 ${\Pi }_0(\mathrm{Disc}(X))\to X\text{.}$ 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 ${\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 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 .from (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 $\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} → is-surjective (Points→Pieces {ℓ} .η x)
pieces-have-points = elim! λ x → inc (x , refl)