module Cat.Functor.Hom.Duality where

Duality of Hom functors🔗

We prove the obvious dualities between functors of opposite categories, and between representable and corepresentable functors.

Hom-from-op :  c  Hom-from (C ^op) c  Hom-into C c
Hom-from-op c = Functor-path  _  refl)  _  refl)

Hom-into-op :  c  Hom-into (C ^op) c  Hom-from C c
Hom-into-op c = Functor-path  _  refl)  _  refl)

  :  {F : Functor C (Sets )}
   Corepresentation F  Representation {C = C ^op} F
corepresentable→co-representable F-corep .rep = F-corep .corep
corepresentable→co-representable F-corep .represents = F-corep .corepresents
  ∘ni path→iso (sym (Hom-into-op _))

  :  {F : Functor (C ^op) (Sets )}
   Representation {C = C} F  Corepresentation F
co-representable→corepresentable F-rep .corep = F-rep .rep
co-representable→corepresentable F-rep .corepresents = F-rep .represents
  ∘ni path→iso (sym (Hom-from-op _))