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-Cat is “cohesive”🔗

We prove that the category Catstrict\strcat admits an adjoint quadruple

Π0DiscΓCodisc \Pi_0 \dashv \id{Disc} \dashv \Gamma \dashv \id{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 Sets\id{Sets}. The left- and right- adjoints to Ob\id{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\id{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-Cat 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 SS to the coproduct of SS-many copies of the point category.

Disc ⊣ Γ🔗

We begin by defining the object set functor.

Γ : Functor (Strict-Cat 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-Cat  )
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 ΓDisc\Gamma \circ \id{Disc}; Since the object set of Disc(X)\id{Disc}(X) is simply XX, 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\id{Disc}(\Gamma(X)) \to X, naturally in XX. Since morphisms in discrete categories are paths, for a map xyx \equiv y (in {- 1 -}), it suffices to assume yy really is xx, and so the identity map suffices.

  adj .counit = NT  x  F x) nat where
    F : (x : Precategory.Ob (Strict-Cat  ))
       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 XX is the strict category with object space XX, and all hom-spaces contractible. The assignment of codiscrete categories extends to a functor SetsCatstrict\sets \to \strcat, where we lift functions to act on object parts and the action on morphisms is trivial.

Codisc : Functor (Sets ) (Strict-Cat  )
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 xHom(,x)x \mapsto \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\hom-sets are definitionally contractible.

module _ {} where
  import Cat.Morphism Cat[ Strict-Cat   , Sets  ] as Nt

  GlobalSections : Functor (Strict-Cat  ) (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\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 Pieces) from Strict-Cat back to Sets. We send a functor FF to its object part, but postcomposing with the map inc which sends an object of D\ca{D} to the connected component it inhabits.

Π₀ : Functor (Strict-Cat 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:Cx, y : \ca{C} are in the same connected component if there is a map r:xyr : x \to y; To show that F0(x)F_0(x) and F0(y)F_0(y) are also in the same connected component, we must give a map F0(x)F0(y)F_0(x) \to F_0(y), but this can be canonically chosen to be F1(r)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 XDisc(Π0(X))\ca{X} \to \id{Disc}(\Pi_0(\ca{X})). We send xx to its connected component, and we must send a map r:xyr : x \to y to an equality between the connected components of xx and yy; 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 Π0(Disc(X))X\Pi_0(\id{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 π0\pi_0 of the product category onto π0\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 Γ(X)Π0(X)\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)