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 CC, we get a natural transformation between F:C→DF : 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 Ξ·:Fβ‡’G\eta : F \Rightarrow G and ΞΈ:Gβ‡’H\theta : G \Rightarrow H, we can show that the assignment x↦ηx∘θxx \mapsto \eta_x \circ \theta_x of β€œcomponentwise compositions” defines a natural transformation Fβ‡’HF \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 .η _

We can then show that these definitions assemble into a category where the objects are functors F,G:C→DF, G : C \to D, and the morphisms are natural transformations F⇒GF \Rightarrow 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 F≑GF \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 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:C→DF : C \to D, the space of functors GG equipped with natural isomorphisms F≅GF \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 ]

The hard part is showing that, given some other functor G:Cβ†’DG : C \to D with a natural isomorphism Fβ‰…GF \cong G, we can give a continuous deformation p:G≑Fp : G \equiv F, such that, over this pp, 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 DD. Since DD 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≅GF \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 (Nat-isoβ†’Iso Fβ‰…G x)

A slightly annoying calculation tells us that pre/post composition with Fβ‰…GF \cong G does in fact turn F1(f)F_1(f) into G1(f)G_1(f); This is because Fβ‰…GF \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₁ {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 Ξ·x∘id∘id=f\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 CΓ—Dβ†’E\mathcal{C} \times \mathcal{D} \to E and the space of functors Cβ†’[D,E]\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 C\mathcal{C} to [J,C][\mathcal{J}, \mathcal{C}] that takes an object x:Cx : \mathcal{C} to the constant functor j↦xj \mapsto x.

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