open import Cat.Functor.Equivalence open import Cat.Instances.Functor open import Cat.Functor.Base open import Cat.Prelude import Cat.Reasoning module Cat.Instances.Functor.Duality where
Duality of functor categoriesπ
The duality involution on categories extends to a βduality involutionβ on functors. However, since this changes the type of the functor β the dual of is β it does not represent an involution on functor categories; Rather, it is an equivalence .
op-functorβ : Functor (Cat[ C , D ] ^op) Cat[ C ^op , D ^op ] op-functorβ .Fβ = Functor.op op-functorβ .Fβ nt .Ξ· = nt .Ξ· op-functorβ .Fβ nt .is-natural x y f = sym (nt .is-natural y x f) op-functorβ .F-id = Nat-path (Ξ» x β refl) op-functorβ .F-β f g = Nat-path Ξ» x β refl op-functor-is-iso : is-precat-iso (op-functorβ {C = C} {D = D}) op-functor-is-iso = isom where open is-precat-iso open is-iso isom : is-precat-iso _ isom .has-is-ff = is-isoβis-equiv ff where ff : is-iso (Fβ op-functorβ) ff .inv nt .Ξ· = nt .Ξ· ff .inv nt .is-natural x y f = sym (nt .is-natural y x f) ff .rinv x = Nat-path Ξ» x β refl ff .linv x = Nat-path Ξ» x β refl isom .has-is-iso = is-isoβis-equiv (iso Functor.op (Ξ» x β Functor-path (Ξ» x β refl) (Ξ» x β refl)) (Ξ» x β F^op^opβ‘F))
This means, in particular, that it is an adjoint equivalence:
op-functor-is-equiv : is-equivalence (op-functorβ {C = C} {D = D}) op-functor-is-equiv = is-precat-isoβis-equivalence op-functor-is-iso op-functorβ : Functor Cat[ C ^op , D ^op ] (Cat[ C , D ] ^op) op-functorβ = is-equivalence.Fβ»ΒΉ op-functor-is-equiv op-functorββ : op-functorβ {C = C} {D = D} Fβ op-functorβ β‘ Id op-functorββ {C = C} {D = D} = Functor-path (Ξ» x β refl) Ξ» {X} {Y} f β Nat-path Ξ» x β (_ D.β f .Ξ· x) D.β _ β‘β¨ D.elimr (lemma {Y = Y}) β©β‘ _ D.β f .Ξ· x β‘β¨ D.eliml (lemma {Y = X}) β©β‘ f .Ξ· x β where module D = Cat.Reasoning D module C = Cat.Reasoning C lemma : β {Y : Functor C D} {x} β coe0β1 (Ξ» i β D.Hom (Fβ Y (transp (Ξ» j β C.Ob) i x)) (Fβ Y (transp (Ξ» j β C.Ob) i x))) D.id β‘ D.id lemma {Y} {x} = from-pathp {A = Ξ» i β D.Hom (Fβ Y (transp (Ξ» j β C.Ob) i x)) (Fβ Y (transp (Ξ» j β C.Ob) i x))} Ξ» i β hcomp (β i) Ξ» where j (i = i0) β D.id j (i = i1) β transport-filler (Ξ» j β D.Hom (Fβ Y x) (Fβ Y x)) D.id (~ j) j (j = i0) β coe0βi (Ξ» j β D.Hom (Fβ Y (transp (Ξ» j β C.Ob) (i β¨ j) x)) (Fβ Y (transp (Ξ» j β C.Ob) (i β¨ j) x))) i D.id module _ {o β oβ² ββ²} {C : Precategory o β} {D : Precategory oβ² ββ²} {F G : Functor C D} where private module CD = Cat.Reasoning Cat[ C , D ] module CopDop = Cat.Reasoning Cat[ C ^op , D ^op ] op-natural-iso : F CD.β G β (Functor.op F) CopDop.β (Functor.op G) op-natural-iso isom = CopDop.make-iso (_=>_.op isom.from) (_=>_.op isom.to) (Nat-path Ξ» x β isom.invl Ξ·β x) (Nat-path Ξ» x β isom.invr Ξ·β x) where module isom = CD._β _ isom