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