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 , we get a natural transformation between 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 and , we can show that the assignment of βcomponentwise compositionsβ defines a natural transformation , which serves as the composite of and .
_β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
We can then show that these definitions assemble into a category where the objects are functors , and the morphisms are natural transformations . This is because natural transformations inherit the identity and associativity laws from the codomain category , 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 between the object mappings, and an identification of morphism parts that lies over , we can identify the functors .
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 is univalent, then so is the category of functors . 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 .
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 is a category, by showing that, for a fixed functor , the space of functors equipped with natural isomorphisms is contractible. The centre of contraction is the straightforward part: We have the canonical choice of .
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 with a natural isomorphism , we can give a continuous deformation , such that, over this , 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 . Since 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 induces a homotopy between the object parts of and :
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 does in fact turn into ; This is because is natural, so we can push it βpastβ the morphism part of 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 .
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 and the space of functors . 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 to that takes an object to the constant functor .
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 _)