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 Cop\mathcal{C}^{\mathrm{op}} on categories extends to a β€œduality involution” FopF^{\mathrm{op}} on functors. However, since this changes the type of the functor β€” the dual of F:Cβ†’DF : \mathcal{C} \to \mathcal{D} is Fop:Cβ†’DF^{\mathrm{op}} : \mathcal{C} \to \mathcal{D} β€” it does not represent an involution on functor categories; Rather, it is an equivalence (βˆ’)op:[C,D]opβ‰…[Cop,Dop](-)^{\mathrm{op}} : [\mathcal{C},\mathcal{D}]^{\mathrm{op}} \cong [\mathcal{C}^{\mathrm{op}},\mathcal{D}^{\mathrm{op}}].

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 = 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 (Ξ» _ β†’ refl) Ξ» f β†’ Nat-path Ξ» x β†’
  Regularity.precise! ((D.id D.∘ f .Ξ· x) D.∘ D.id β‰‘βŸ¨ cat! D βŸ©β‰‘ f .Ξ· x ∎)
  where
    module D = Cat.Reasoning D

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