open import Cat.Functor.Equivalence
open import Cat.Instances.Functor
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

private variable
o β : Level
C D : Precategory o β

open Functor
open _=>_

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 = trivial!
op-functorβ .F-β f g = trivial!

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 = trivial!
ff .linv x = trivial!
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 (Ξ» _ β refl) Ξ» f β ext Ξ» x β
Regularity.precise! ((D.id D.β f .Ξ· x) D.β D.id β‘β¨ cat! D β©β‘ f .Ξ· x β)
where
module D = Cat.Reasoning D