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 CC, we get a natural transformation between F:CDF : 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 η:FG\eta : F \To G and θ:GH\theta : G \To H, we can show that the assignment xηxθxx \mapsto \eta_x \circ \theta_x of “componentwise compositions” defines a natural transformation FHF \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:CDF, G : C \to D, and the morphisms are natural transformations FGF \To G. This is because natural transformations inherit the identity and associativity laws from the codomain category DD, 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:F0(x)G0(x)p : F_0(x) \equiv G_0(x) between the object mappings, and an identification of morphism parts that lies over pp, we can identify the functors FGF \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 DD is univalent, then so is the category of functors [C,D][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 DD.

  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][C,D] is a category, by showing that, for a fixed functor F:CDF : C \to D, the space of functors GG equipped with natural isomorphisms FGF \cong G is contractible. The centre of contraction is the straightforward part: We have the canonical choice of (F,id)(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:CDG : C \to D with a natural isomorphism FGF \cong G, we can give a continuous deformation p:GFp : G \equiv F, such that, over this pp, 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 DD. Since DD is a category, path→iso is an equivalence; The lemmas we need then follow from equivalences having sections.

      :  x  path→iso (iso→path DisCat (Nat-iso→Iso F≅G _)) .D._≅
             F≅G .to .η x
    ptoi-to x = ap  e  e .D._≅
      (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 FGF \cong G induces a homotopy between the object parts of FF and GG:

    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 FGF \cong G does in fact turn F1(f)F_1(f) into G1(f)G_1(f); This is because FGF \cong G is natural, so we can push it “past” the morphism part of FF so that the two halves of the isomorphism annihilate.

      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.∘ 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 ηxidid=f\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]
    module F = Functor F
    module G = Functor G


    : (eta : F => G)
     (∀ x (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 ( _ _ _))) 
      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 =
        { inv      = eps
        ; inverses =
            { invl = Nat-path λ x  invs x .invl
            ; invr = Nat-path λ x  invs x .invr


There is an equivalence between the spaces of bifunctors C×CatDE\ca{C} \times_\cat \ca{D} \to E and the space of functors C[D,E]\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.₁ .η y E.∘ F₁ (F.₀ x) ≡⟨ E.elimr (F-id (F.₀ x)) 
      F.₁ .η y                     ≡⟨  i  F.F-id i .η y)                              

  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′))