open import Cat.Instances.Product
open import Cat.Univalent using (is-category)
open import Cat.Prelude

import Cat.Reasoning

open Precategory
open Functor
open _=>_

module Cat.Instances.Functor where

private variable
  o h o₁ h₁ o₂ h₂ : Level
  C D E : Precategory o h
  F G : Functor C D

Functor (pre)categories🔗

By assigning the identity morphism to every object in $C$, we get a natural transformation between $F : C \to D$ and itself.

idnt : {F : Functor C D} → F => F
idnt {C = C} {D = D} .η x = D .id
idnt {C = C} {D = D} .is-natural x y f = D .idl _ ∙ sym (D .idr _)

Given two natural transformations $\eta : F \To G$ and $\theta : G \To H$, we can show that the assignment $x \mapsto \eta_x \circ \theta_x$ of “componentwise compositions” defines a natural transformation $F \To H$, which serves as the composite of $\eta$ and $\theta$.

_∘nt_ : {F G H : Functor C D} → G => H → F => G → F => H
_∘nt_ {C = C} {D = D} {F} {G} {H} f g = nat where
  module D = Precategory D

  nat : F => H
  nat .η x = f .η _ D.∘ g .η _

We can then show that these definitions assemble into a category where the objects are functors $F, G : C \to D$, and the morphisms are natural transformations $F \To G$. This is because natural transformations inherit the identity and associativity laws from the codomain category $D$, and since hom-sets are sets, is-natural does not matter.

module _ {o₁ h₁ o₂ h₂} (C : Precategory o₁ h₁) (D : Precategory o₂ h₂) where
  open Precategory

  Cat[_,_] : Precategory (o₁ ⊔ o₂ ⊔ h₁ ⊔ h₂) (o₁ ⊔ h₁ ⊔ h₂)
  Cat[_,_] .Ob = Functor C D
  Cat[_,_] .Hom F G = F => G
  Cat[_,_] .id = idnt
  Cat[_,_] ._∘_ = _∘nt_

All of the properties that make up a Precategory follow from the characterisation of equalities in natural transformations: They are a set, and equality of the components determines equality of the transformation.

  Cat[_,_] .Hom-set F G = Nat-is-set
  Cat[_,_] .idr f = Nat-path λ x → D .idr _
  Cat[_,_] .idl f = Nat-path λ x → D .idl _
  Cat[_,_] .assoc f g h = Nat-path λ x → D .assoc _ _ _

Before moving on, we prove the following lemma which characterises equality in Functor (between definitionally equal categories). Given an identification $p : F_0(x) \equiv G_0(x)$ between the object mappings, and an identification of morphism parts that lies over $p$, we can identify the functors $F \equiv G$.

Functor-path : {F G : Functor C D}
         → (p0 : ∀ x → F₀ F x ≡ F₀ G x)
         → (p1 : ∀ {x y} (f : C .Hom x y)
               → PathP (λ i → D .Hom (p0 x i) (p0 y i)) (F₁ F f) (F₁ G f))
         → F ≡ G
Functor-path p0 p1 i .F₀ x = p0 x i
Functor-path p0 p1 i .F₁ f = p1 f i

Functor categories🔗

When the codomain category $D$ is univalent, then so is the category of functors $[C,D]$. Essentially, this can be read as saying that “naturally isomorphic functors are identified”. We begin by proving that the components of a natural isomorphism (a natural transformation with natural inverse) are themselves isomorphisms in $D$.

  Nat-iso→Iso : F [C,D].≅ G → ∀ x → F₀ F x D.≅ F₀ G x
  Nat-iso→Iso natiso x =
    D.make-iso (to .η x) (from .η x)
      (λ i → invl i .η x) (λ i → invr i .η x)
    where open [C,D]._≅_ natiso

We can now prove that $[C,D]$ is a category, by showing that, for a fixed functor $F : C \to D$, the space of functors $G$ equipped with natural isomorphisms $F \cong G$ is contractible. The centre of contraction is the straightforward part: We have the canonical choice of $(F, id)$.

  Functor-is-category : is-category D → is-category Cat[ C , D ]
  Functor-is-category _ F .centre = F , id-iso

The hard part is showing that, given some other functor $G : C \to D$ with a natural isomorphism $F \cong G$, we can give a continuous deformation $p : G \equiv F$, such that, over this $p$, the given isomorphism looks like the identity.

  Functor-is-category DisCat F .paths (G , F≅G) = Σ-pathp F≡G id≡F≅G where

The first thing we must note is that we can recover the components of a natural isomorphism while passing to/from paths in $D$. Since $D$ is a category, path→iso is an equivalence; The lemmas we need then follow from equivalences having sections.

    ptoi-to
      : ∀ x → path→iso (iso→path DisCat (Nat-iso→Iso F≅G _)) .D._≅_.to
            ≡ F≅G .to .η x
    ptoi-to x = ap (λ e → e .D._≅_.to)
      (equiv→section (path→iso-is-equiv DisCat) _)

    ptoi-from : ∀ x → path→iso (iso→path DisCat (Nat-iso→Iso F≅G _)) .D._≅_.from
              ≡ F≅G .from .η x
    ptoi-from x = ap (λ e → e .D._≅_.from)
      (equiv→section (path→iso-is-equiv DisCat) _)

We can then show that the natural isomorphism $F \cong G$ induces a homotopy between the object parts of $F$ and $G$:

    F₀≡G₀ : ∀ x → F₀ F x ≡ F₀ G x
    F₀≡G₀ x = iso→path DisCat (Nat-iso→Iso F≅G x)

A slightly annoying calculation tells us that pre/post composition with $F \cong G$ does in fact turn $F_1(f)$ into $G_1(f)$; This is because $F \cong G$ is natural, so we can push it “past” the morphism part of $F$ so that the two halves of the isomorphism annihilate.

    abstract
      F₁≡G₁ : ∀ {x y} {f : C .Hom x y}
            → PathP (λ i → D.Hom (F₀≡G₀ x i) (F₀≡G₀ y i)) (F₁ F f) (F₁ G f)
      F₁≡G₁ {x = x} {y} {f} = Hom-pathp (
        _ D.∘ F .F₁ f D.∘ _                           ≡⟨ (λ i → ptoi-to _ i D.∘ F .F₁ f D.∘ ptoi-from _ i) ⟩≡
        F≅G .to .η y D.∘ F .F₁ f D.∘ F≅G .from .η x   ≡⟨ ap₂ D._∘_ refl (sym (F≅G .from .is-natural _ _ _)) ∙ D.assoc _ _ _ ⟩≡
        (F≅G .to .η y D.∘ F≅G .from .η y) D.∘ G .F₁ f ≡⟨ ap₂ D._∘_ (λ i → F≅G .invl i .η y) refl ⟩≡
        D.id D.∘ G .F₁ f                              ≡⟨ solve D ⟩≡
        G .F₁ f                                       ∎)

    F≡G : F ≡ G
    F≡G = Functor-path F₀≡G₀ λ f → F₁≡G₁

Putting these homotopies together defines a path F≡G. It remains to show that, over this path, the natural isomorphism we started with is homotopic to the identity; Equality of isomorphisms and natural transformations are both tested componentwise, so we can “push down” the relevant equalities to the level of families of morphisms; By computation, all we have to show is that $\eta{}_x \circ \id{id} \circ \id{id} = f$.

    id≡F≅G : PathP (λ i → F ≅ F≡G i) id-iso F≅G
    id≡F≅G = ≅-pathp refl F≡G
      (Nat-pathp refl F≡G
        λ x → Hom-pathp
          (  ap₂ D._∘_ (ptoi-to _) refl
          ·· ap₂ D._∘_ refl (ap₂ D._∘_ refl (transport-refl _) ∙ D.idl _)
          ·· D.idr _))

A useful lemma is that if you have a natural transformation where each component is an isomorphism, the evident inverse transformation is natural too, thus defining an inverse to Nat-iso→Iso defined above.

module _ {C : Precategory o h} {D : Precategory o₁ h₁} {F G : Functor C D} where
  import Cat.Reasoning D as D
  import Cat.Reasoning Cat[ C , D ] as [C,D]
  private
    module F = Functor F
    module G = Functor G

  open D.is-invertible

  componentwise-invertible→invertible
    : (eta : F => G)
    → (∀ x → D.is-invertible (eta .η x))
    → [C,D].is-invertible eta
  componentwise-invertible→invertible eta invs = are-invs where
    module eta = _=>_ eta

    eps : G => F
    eps .η x = invs x .inv
    eps .is-natural x y f =
      invs y .inv D.∘ G.₁ f                             ≡⟨ ap₂ D._∘_ refl (sym (D.idr _) ∙ ap (G.₁ f D.∘_) (sym (invs x .invl))) ⟩≡
      invs y .inv D.∘ G.₁ f D.∘ eta.η x D.∘ invs x .inv ≡⟨ ap₂ D._∘_ refl (D.extendl (sym (eta.is-natural _ _ _))) ⟩≡
      invs y .inv D.∘ eta.η y D.∘ F.₁ f D.∘ invs x .inv ≡⟨ D.cancell (invs y .invr) ⟩≡
      F.₁ f D.∘ invs x .inv ∎

    are-invs : [C,D].is-invertible eta
    are-invs =
      record
        { inv      = eps
        ; inverses =
          record
            { invl = Nat-path λ x → invs x .invl
            ; invr = Nat-path λ x → invs x .invr
            }
        }

Currying🔗

There is an equivalence between the spaces of bifunctors $\ca{C} \times_\cat \ca{D} \to E$ and the space of functors $\ca{C} \to [\ca{D},E]$. We refer to the image of a functor under this equivalence as its exponential transpose, and we refer to the map in the “forwards” direction (as in the text above) as currying:

Curry : Functor (C ×Cat D) E → Functor C Cat[ D , E ]
Curry {C = C} {D = D} {E = E} F = curried where
  open import Cat.Functor.Bifunctor {C = C} {D = D} {E = E} F

  curried : Functor C Cat[ D , E ]
  curried .F₀ = Right
  curried .F₁ x→y = NT (λ f → first x→y) λ x y f →
       sym (F-∘ F _ _)
    ·· ap (F₁ F) (Σ-pathp (C .idr _ ∙ sym (C .idl _)) (D .idl _ ∙ sym (D .idr _)))
    ·· F-∘ F _ _
  curried .F-id = Nat-path λ x → F-id F
  curried .F-∘ f g = Nat-path λ x →
    ap (λ x → F₁ F (_ , x)) (sym (D .idl _)) ∙ F-∘ F _ _

Uncurry : Functor C Cat[ D , E ] → Functor (C ×Cat D) E
Uncurry {C = C} {D = D} {E = E} F = uncurried where
  import Cat.Reasoning C as C
  import Cat.Reasoning D as D
  import Cat.Reasoning E as E
  module F = Functor F

  uncurried : Functor (C ×Cat D) E
  uncurried .F₀ (c , d) = F₀ (F.₀ c) d
  uncurried .F₁ (f , g) = F.₁ f .η _ E.∘ F₁ (F.₀ _) g

  uncurried .F-id {x = x , y} = path where abstract
    path : E ._∘_ (F.₁ (C .id) .η y) (F₁ (F.₀ x) (D .id)) ≡ E .id
    path =
      F.₁ C.id .η y E.∘ F₁ (F.₀ x) D.id ≡⟨ E.elimr (F-id (F.₀ x)) ⟩≡
      F.₁ C.id .η y                     ≡⟨ (λ i → F.F-id i .η y) ⟩≡
      E.id                              ∎

  uncurried .F-∘ (f , g) (f′ , g′) = path where abstract
    path : uncurried .F₁ (f C.∘ f′ , g D.∘ g′)
         ≡ uncurried .F₁ (f , g) E.∘ uncurried .F₁ (f′ , g′)
    path =
      F.₁ (f C.∘ f′) .η _ E.∘ F₁ (F.₀ _) (g D.∘ g′)                       ≡˘⟨ E.pulll (λ i → F.F-∘ f f′ (~ i) .η _) ⟩≡˘
      F.₁ f .η _ E.∘ F.₁ f′ .η _ E.∘ F₁ (F.₀ _) (g D.∘ g′)                ≡⟨ (λ i → F.₁ f .η _ E.∘ F.₁ f′ .η _ E.∘ F-∘ (F.₀ _) g g′ i) ⟩≡
      F.₁ f .η _ E.∘ F.₁ f′ .η _ E.∘ F₁ (F.₀ _) g E.∘ F₁ (F.₀ _) g′       ≡⟨ solve E ⟩≡
      F.₁ f .η _ E.∘ (F.₁ f′ .η _ E.∘ F₁ (F.₀ _) g) E.∘ F₁ (F.₀ _) g′     ≡⟨ ap (λ e → _ E.∘ e E.∘ _) (F.₁ f′ .is-natural _ _ _) ⟩≡
      F.₁ f .η _ E.∘ (F₁ (F.₀ _) g E.∘ F.₁ f′ .η _) E.∘ F₁ (F.₀ _) g′     ≡⟨ solve E ⟩≡
      ((F.₁ f .η _ E.∘ F₁ (F.₀ _) g) E.∘ (F.₁ f′ .η _ E.∘ F₁ (F.₀ _) g′)) ∎