open import 1Lab.Path.Cartesian

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

import Cat.Functor.Reasoning as Fr
import Cat.Reasoning

open Precategory
open Functor
open _=>_

module Cat.Instances.Functor where

private variable
o h oβ hβ oβ hβ : Level
B 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 \Rightarrow G$ and $\theta : G \Rightarrow H$, we can show that the assignment $x \mapsto \eta_x \circ \theta_x$ of βcomponentwise compositionsβ defines a natural transformation $F \Rightarrow 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
module βnt where
module D = Cat.Reasoning D

nat : F => H
nat .Ξ· x = f .Ξ· _ D.β g .Ξ· _

    nat .is-natural x y h =
(f .Ξ· y D.β g .Ξ· y) D.β F.β h  β‘β¨ D.pullr (g .is-natural _ _ _) β©β‘
f .Ξ· y D.β (G.β h D.β g .Ξ· x)  β‘β¨ D.extendl (f .is-natural _ _ _) β©β‘
H.β h  D.β f .Ξ· _ D.β g .Ξ·  _  β
where
module C = Precategory C
module F = Functor F
module G = Functor G
module H = Functor H

infixr 40 _βnt_
{-# DISPLAY βnt.nat f g = f βnt 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 \Rightarrow 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-path {C = C} {D = D} {F = F} {G = G} p0 p1 i .F-id =
is-propβpathp (Ξ» j β D .Hom-set _ _ (p1 (C .id) j) (D .id))
(F-id F) (F-id G) i
Functor-path {C = C} {D = D} {F = F} {G = G} p0 p1 i .F-β f g =
is-propβpathp (Ξ» i β D .Hom-set _ _ (p1 (C ._β_ f g) i) (D ._β_ (p1 f i) (p1 g i)))
(F-β F f g) (F-β G f g) i

Functor-pathp
: {C : I β Precategory o h} {D : I β Precategory oβ hβ}
{F : Functor (C i0) (D i0)} {G : Functor (C i1) (D i1)}
β (p0 : β (p : β i β C i .Ob) β PathP (Ξ» i β D i .Ob) (Fβ F (p i0)) (Fβ G (p i1)))
β (p1 : β {x y : β i β _}
β (r : β i β C i .Hom (x i) (y i))
β PathP (Ξ» i β D i .Hom (p0 x i) (p0 y i))
(Fβ F (r i0)) (Fβ G (r i1)))
β PathP (Ξ» i β Functor (C i) (D i)) F G
Functor-pathp {C = C} {D} {F} {G} p0 p1 = fn where
cob : I β Type _
cob = Ξ» i β C i .Ob

exth
: β i j (x y : C i .Ob) (f : C i .Hom x y)
β C i .Hom (coe cob i i x) (coe cob i i y)
exth i j x y f =
comp (Ξ» j β C i .Hom (coeiβi cob i x (~ j β¨ i)) (coeiβi cob i y (~ j β¨ i)))
((~ i β§ ~ j) β¨ (i β§ j))
Ξ» where
k (k = i0) β f
k (i = i0) (j = i0) β f
k (i = i1) (j = i1) β f

actm
: β i (x y : C i .Ob) f
β D i .Hom (p0 (Ξ» j β coe cob i j x) i) (p0 (Ξ» j β coe cob i j y) i)
actm i x y f =
p1 {Ξ» j β coe cob i j x} {Ξ» j β coe cob i j y}
(Ξ» j β coe (Ξ» j β C j .Hom (coe cob i j x) (coe cob i j y)) i j (exth i j x y f))
i

fn : PathP (Ξ» i β Functor (C i) (D i)) F G
fn i .Fβ x =
p0 (Ξ» j β coe cob i j x)
i
fn i .Fβ {x} {y} f = actm i x y f
fn i .F-id {x} =
hcomp (β i) Ξ» where
j (i = i0) β D i .Hom-set (F .Fβ x) (F .Fβ x) (F .Fβ (C i .id)) (D i .id) base (F .F-id) j
j (i = i1) β D i .Hom-set (G .Fβ x) (G .Fβ x) (G .Fβ (C i .id)) (D i .id) base (G .F-id) j
j (j = i0) β base
where
base = coe0βi (Ξ» i β (x : C i .Ob) β actm i x x (C i .id) β‘ D i .id) i
(Ξ» _ β F .F-id) x
fn i .F-β {x} {y} {z} f g =
hcomp (β i) Ξ» where
j (i = i0) β D i .Hom-set (F .Fβ x) (F .Fβ z) _ _ base (F .F-β f g) j
j (i = i1) β D i .Hom-set (G .Fβ x) (G .Fβ z) _ _ base (G .F-β f g) j
j (j = i0) β base
where
base = coe0βi (Ξ» i β (x y z : C i .Ob) (f : C i .Hom y z) (g : C i .Hom x y)
β actm i x z (C i ._β_ f g)
β‘ D i ._β_ (actm i y z f) (actm i x y g)) i
(Ξ» _ _ _ β F .F-β) x y z f g


## 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$.

module _ {C : Precategory o h} {D : Precategory oβ hβ} where
import Cat.Morphism D as D
import Cat.Morphism Cat[ C , D ] as [C,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)$.

module _ {C : Precategory oβ hβ} {D : Precategory oβ hβ} where
import Cat.Reasoning Cat[ C , D ] as [C,D]
import Cat.Reasoning D as D
open [C,D]

  Functor-is-category : is-category D β is-category Cat[ C , D ]


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 = functor-cat 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.

    open Cat.Univalent.Univalent DisCat
using (isoβpath ; isoβpathβiso ; pathβisoβpath ; Hom-pathp-iso ; Hom-pathp-reflr-iso)

module _ {F G} (FβG : _) where
ptoi-to
: β x β pathβiso (isoβpath (Nat-isoβIso FβG _)) .D._β_.to β‘ FβG .to .Ξ· x
ptoi-to x = ap (Ξ» e β e .D._β_.to) (isoβpathβiso (Nat-isoβIso FβG x))

ptoi-from : β x β pathβiso (isoβpath (Nat-isoβIso FβG _)) .D._β_.from
β‘ FβG .from .Ξ· x
ptoi-from x = ap (Ξ» e β e .D._β_.from) (isoβpathβiso (Nat-isoβIso FβG x))


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

      Fββ‘Gβ : β {x y} (f : C .Hom x y)
β PathP (Ξ» i β D.Hom (Fββ‘Gβ x i) (Fββ‘Gβ y i)) (F .Fβ {x} {y} f) (G .Fβ {x} {y} f)
Fββ‘Gβ {x = x} {y} f = Hom-pathp-iso $(D.extendl (Fβ G .to .is-natural x y f) β D.elimr (Fβ G .invl Ξ·β x)) Fβ‘G : F β‘ G Fβ‘G = Functor-path Fββ‘Gβ Ξ» f β Fββ‘Gβ f  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 \mathrm{id}_{} \circ \mathrm{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-reflr-iso (D.idr _)

functor-cat : is-category Cat[ C , D ]
functor-cat .to-path = Fβ‘G
functor-cat .to-path-over = idβ‘FβG


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! (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.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 $\mathcal{C} \times \mathcal{D} \to E$ and the space of functors $\mathcal{C} \to [\mathcal{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 ΓαΆ 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 ΓαΆ 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 ΓαΆ 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β²) β            β‘β¨ ap! (F-β (F.β _) _ _) β©β‘
F.β f .Ξ· _ E.β F.β fβ² .Ξ· _ E.β Fβ (F.β _) g E.β Fβ (F.β _) gβ²       β‘β¨ cat! E β©β‘
F.β f .Ξ· _ E.β β F.β fβ² .Ξ· _ E.β Fβ (F.β _) g β E.β Fβ (F.β _) gβ²   β‘β¨ ap! (F.β fβ² .is-natural _ _ _) β©β‘
F.β f .Ξ· _ E.β (Fβ (F.β _) g E.β F.β fβ² .Ξ· _) E.β Fβ (F.β _) gβ²     β‘β¨ cat! E β©β‘
((F.β f .Ξ· _ E.β Fβ (F.β _) g) E.β (F.β fβ² .Ξ· _ E.β Fβ (F.β _) gβ²)) β


## Constant Diagramsπ

There is a functor from $\mathcal{C}$ to $[\mathcal{J}, \mathcal{C}]$ that takes an object $x : \mathcal{C}$ to the constant functor $j \mapsto x$.

module _ {o β o' β'} {C : Precategory o β} {J : Precategory o' β'} where
private module C = Precategory C
private module J = Precategory J

  ConstD : Functor C Cat[ J , C ]
ConstD .Fβ x = Const x
ConstD .Fβ f = const-nt f
ConstD .F-id = Nat-path (Ξ» _ β refl)
ConstD .F-β f g = Nat-path (Ξ» _ β refl)

PSh : β ΞΊ {o β} β Precategory o β β Precategory _ _
PSh ΞΊ C = Cat[ C ^op , Sets ΞΊ ]

Fβ-assoc
: β {o β oβ² ββ² oβ²β² ββ²β² oβ ββ}
{C : Precategory o β} {D : Precategory oβ² ββ²} {E : Precategory oβ²β² ββ²β²} {F : Precategory oβ ββ}
{F : Functor E F} {G : Functor D E} {H : Functor C D}
β F Fβ (G Fβ H) β‘ (F Fβ G) Fβ H
Fβ-assoc = Functor-path (Ξ» x β refl) Ξ» x β refl

Fβ-idl
: β {oβ²β² ββ²β² oβ ββ}
{E : Precategory oβ²β² ββ²β²} {Eβ² : Precategory oβ ββ}
{F : Functor E Eβ²}
β Id Fβ F β‘ F
Fβ-idl = Functor-path (Ξ» x β refl) Ξ» x β refl

Fβ-idr
: β {oβ²β² ββ²β² oβ ββ}
{E : Precategory oβ²β² ββ²β²} {Eβ² : Precategory oβ ββ}
{F : Functor E Eβ²}
β F Fβ Id β‘ F
Fβ-idr = Functor-path (Ξ» x β refl) Ξ» x β refl

module
_ {o β oβ² ββ² oβ²β² ββ²β²}
{C : Precategory o β} {D : Precategory oβ² ββ²} {E : Precategory oβ²β² ββ²β²}
where
private
module DE = Cat.Reasoning Cat[ D , E ]
module CE = Cat.Reasoning Cat[ C , E ]

Fβ-iso-l : {F Fβ² : Functor D E} {G : Functor C D}
β F DE.β Fβ² β (F Fβ G) CE.β (Fβ² Fβ G)
Fβ-iso-l {F} {Fβ²} {G} isom =
CE.make-iso to from
(Nat-path Ξ» x β isom.invl Ξ·β _)
(Nat-path Ξ» x β isom.invr Ξ·β _)
where
module isom = DE._β_ isom
to : (F Fβ G) => (Fβ² Fβ G)
to .Ξ· _ = isom.to .Ξ· _
to .is-natural _ _ _ = isom.to .is-natural _ _ _

from : (Fβ² Fβ G) => (F Fβ G)
from .Ξ· _ = isom.from .Ξ· _
from .is-natural _ _ _ = isom.from .is-natural _ _ _

module
_ {o β oβ² ββ²}
{C : Precategory o β} {D : Precategory oβ² ββ²}
where

private
module DD = Cat.Reasoning Cat[ D , D ]
module CD = Cat.Reasoning Cat[ C , D ]
module D = Cat.Reasoning D
module C = Cat.Reasoning C

natural-inverses : {F G : Functor C D} β F => G β G => F β Type _
natural-inverses = CD.Inverses

is-natural-invertible : {F G : Functor C D} β F => G β Type _
is-natural-invertible = CD.is-invertible

natural-iso : (F G : Functor C D) β Type _
natural-iso F G = F CD.β G

module natural-inverses {F G : Functor C D} {Ξ± : F => G} {Ξ² : G => F} (inv : natural-inverses Ξ± Ξ²) =
CD.Inverses inv
module is-natural-invertible {F G : Functor C D} {Ξ± : F => G} (inv : is-natural-invertible Ξ±) =
CD.is-invertible inv
module natural-iso {F G : Functor C D} (eta : natural-iso F G) = CD._β_ eta

idni : natural-iso F F
idni = CD.id-iso

_niβ_ : β {F G H : Functor C D}
β natural-iso F G β natural-iso G H
β natural-iso F H
_niβ_ = CD._βIso_

_niβ»ΒΉ : β {F G : Functor C D} β natural-iso F G β natural-iso G F
_niβ»ΒΉ = CD._Isoβ»ΒΉ

Fβ-iso-id-l
: {F : Functor D D} {G : Functor C D}
β F DD.β Id β (F Fβ G) CD.β G
Fβ-iso-id-l {F} {G} isom = subst ((F Fβ G) CD.β_) Fβ-idl (Fβ-iso-l isom)

record make-natural-iso (F G : Functor C D) : Type (o β β β ββ²) where
no-eta-equality
field
eta : β x β D.Hom (F .Fβ x) (G .Fβ x)
inv : β x β D.Hom (G .Fβ x) (F .Fβ x)
etaβinv : β x β eta x D.β inv x β‘ D.id
invβeta : β x β inv x D.β eta x β‘ D.id
natural : β x y f β G .Fβ f D.β eta x β‘ eta y D.β F .Fβ f

to-natural-inverses
: {F G : Functor C D} {Ξ± : F => G} {Ξ² : G => F}
β (β x β Ξ± .Ξ· x D.β Ξ² .Ξ· x β‘ D.id)
β (β x β Ξ² .Ξ· x D.β Ξ± .Ξ· x β‘ D.id)
β natural-inverses Ξ± Ξ²
to-natural-inverses p q =
CD.make-inverses (Nat-path p) (Nat-path q)

to-is-natural-invertible
: {F G : Functor C D} {Ξ± : F => G}
β (Ξ² : G => F)
β (β x β Ξ± .Ξ· x D.β Ξ² .Ξ· x β‘ D.id)
β (β x β Ξ² .Ξ· x D.β Ξ± .Ξ· x β‘ D.id)
β is-natural-invertible Ξ±
to-is-natural-invertible Ξ² p q = CD.make-invertible Ξ² (Nat-path p) (Nat-path q)

to-natural-iso : {F G : Functor C D} β make-natural-iso F G β F CD.β G
to-natural-iso {F = F} {G = G} x = isom where
open CD._β_
open CD.Inverses
open make-natural-iso x
module F = Functor F
module G = Functor G

isom : F CD.β G
isom .to .Ξ· = eta
isom .to .is-natural x y f = sym (natural _ _ _)
isom .from .Ξ· = inv
isom .from .is-natural x y f =
inv y D.β β G.β f β                     β‘β¨ ap! (sym (D.idr _) β ap (G.β f D.β_) (sym (etaβinv x))) β©β‘
inv y D.β β G.β f D.β eta x D.β inv x β β‘β¨ ap! (D.extendl (natural _ _ _)) β©β‘
inv y D.β eta y D.β F.β f D.β inv x     β‘β¨ D.cancell (invβeta y) β©β‘
F.β f D.β inv x β
isom .inverses .invl = Nat-path etaβinv
isom .inverses .invr = Nat-path invβeta

natural-inversesβinverses
: β {Ξ± : F => G} {Ξ² : G => F}
β natural-inverses Ξ± Ξ²
β β x β D.Inverses (Ξ± .Ξ· x) (Ξ² .Ξ· x)
natural-inversesβinverses inv x =
D.make-inverses
(CD.Inverses.invl inv Ξ·β x)
(CD.Inverses.invr inv Ξ·β x)

is-natural-invertibleβinvertible
: β {Ξ± : F => G}
β is-natural-invertible Ξ±
β β x β D.is-invertible (Ξ± .Ξ· x)
is-natural-invertibleβinvertible inv x =
D.make-invertible
(CD.is-invertible.inv inv .Ξ· x)
(CD.is-invertible.invl inv Ξ·β x)
(CD.is-invertible.invr inv Ξ·β x)

is-natural-invertibleβnatural-iso
: β {Ξ± : F => G}
β is-natural-invertible Ξ±
β natural-iso F G
is-natural-invertibleβnatural-iso nat-inv =
CD.invertibleβiso _ nat-inv

natural-isoβis-natural-invertible
: (i : natural-iso F G)
β is-natural-invertible (natural-iso.to i)
natural-isoβis-natural-invertible i =
CD.isoβinvertible i

open _=>_

_ni^op : natural-iso F G β natural-iso (Functor.op F) (Functor.op G)
_ni^op Ξ± =
Cat.Reasoning.make-iso _
(_=>_.op (natural-iso.from Ξ±))
(_=>_.op (natural-iso.to Ξ±))
(Nat-path Ξ» j β natural-iso.invl Ξ± Ξ·β _)
(Nat-path Ξ» j β natural-iso.invr Ξ± Ξ·β _)

module _
{o β oβ² ββ² oβ ββ}
{C : Precategory o β}
{D : Precategory oβ² ββ²}
{E : Precategory oβ ββ}
where
private
de = Cat[ D , E ]
cd = Cat[ C , D ]
open Cat.Reasoning using (to ; from)
open Cat.Univalent

whisker-path-left
: β {G Gβ² : Functor D E} {F : Functor C D}
(ecat : is-category de)
β (p : Cat.Reasoning._β_ de G Gβ²) β β {x}
β pathβiso {C = E} (Ξ» i β (Univalent.isoβpath ecat p i Fβ F) .Fβ x) .to
β‘ p .to .Ξ· (Fβ F x)
whisker-path-left {G} {Gβ²} {F} p =
de.J-iso
(Ξ» B isom β β {x} β pathβiso {C = E} (Ξ» i β Fβ (de.isoβpath isom i Fβ F) x) .to β‘ isom .to .Ξ· (Fβ F x))
Ξ» {x} β ap (Ξ» e β pathβiso {C = E} e .to)
(Ξ» i j β de.isoβpath-id {a = G} i j .Fβ (Fβ F x))
β transport-refl _
where module de = Univalent p

whisker-path-right
: β {G : Functor D E} {F Fβ² : Functor C D}
(cdcat : is-category cd)
β (p : Cat.Reasoning._β_ cd F Fβ²) β β {x}
β pathβiso {C = E} (Ξ» i β Fβ G (Univalent.isoβpath cdcat p i .Fβ x)) .from
β‘ G .Fβ (p .from .Ξ· x)
whisker-path-right {G} {Gβ²} {F} cdcat =
cd.J-iso
(Ξ» B isom β β {x} β pathβiso {C = E} (Ξ» i β Fβ G (cd.isoβpath isom i .Fβ x)) .from β‘ G .Fβ (isom .from .Ξ· x))
Ξ» {x} β ap (Ξ» e β pathβiso {C = E} e .from)
(Ξ» i j β G .Fβ (cd.isoβpath-id {a = Gβ²} i j .Fβ x))
β transport-refl _ β sym (G .F-id)
where module cd = Univalent cdcat

module _ {o β ΞΊ} {C : Precategory o β} where
open Functor
open _=>_

natural-iso-to-is-equiv
: {F G : Functor C (Sets ΞΊ)}
β (eta : natural-iso F G)
β β x β is-equiv (natural-iso.to eta .Ξ· x)
natural-iso-to-is-equiv eta x =
is-isoβis-equiv $iso (natural-iso.from eta .Ξ· x) (Ξ» x i β natural-iso.invl eta i .Ξ· _ x) (Ξ» x i β natural-iso.invr eta i .Ξ· _ x) natural-iso-from-is-equiv : {F G : Functor C (Sets ΞΊ)} β (eta : natural-iso F G) β β x β is-equiv (natural-iso.from eta .Ξ· x) natural-iso-from-is-equiv eta x = is-isoβis-equiv$
iso (natural-iso.to eta .Ξ· x)
(Ξ» x i β natural-iso.invr eta i .Ξ· _ x)
(Ξ» x i β natural-iso.invl eta i .Ξ· _ x)

natural-isoβequiv
: {F G : Functor C (Sets ΞΊ)}
β (eta : natural-iso F G)
β β x β β£ F .Fβ x β£ β β£ G .Fβ x β£
natural-isoβequiv eta x =
natural-iso.to eta .Ξ· x ,
natural-iso-to-is-equiv eta x

module _ where
open Cat.Reasoning

-- [TODO: Reed M, 14/03/2023] Extend the coherence machinery to handle natural
-- isos.
ni-assoc : {F : Functor D E} {G : Functor C D} {H : Functor B C}
β natural-iso (F Fβ G Fβ H) ((F Fβ G) Fβ H)
ni-assoc {E = E} = to-natural-iso Ξ» where
.make-natural-iso.eta _ β E .id
.make-natural-iso.inv _ β E .id
.make-natural-iso.etaβinv _ β E .idl _
.make-natural-iso.invβeta _ β E .idl _
.make-natural-iso.natural _ _ _ β E .idr _ β sym (E .idl _)