open import Cat.Instances.Functor.Duality
open import Cat.Instances.Functor
open import Cat.Prelude

import Cat.Reasoning

module Cat.Diagram.Duals {o h} (C : Precategory o h) where

# Dualities of diagramsš

Following Hu and Carette, weāve opted to have different concrete definitions for diagrams and their opposites. In particular, we have the following pairs of āredundantā definitions:

• Products and coproducts
• Pullbacks and pushouts
• Equalisers and coequalisers
• Terminal objects and initial objects

For all four of the above pairs, we have that one in $C$ is the other in $C\op$. We prove these correspondences here:

## Co/productsš

import Cat.Diagram.Product (C ^op) as Co-prod
import Cat.Diagram.Coproduct C as Coprod

is-co-productāis-coproduct
: ā {A B P} {i1 : C.Hom A P} {i2 : C.Hom B P}
ā Co-prod.is-product i1 i2 ā Coprod.is-coproduct i1 i2
is-co-productāis-coproduct isp =
record
{ [_,_]      = isp.āØ_,_ā©
; ināāfactor = isp.Ļāāfactor
; ināāfactor = isp.Ļāāfactor
; unique     = isp.unique
}
where module isp = Co-prod.is-product isp

is-coproductāis-co-product
: ā {A B P} {i1 : C.Hom A P} {i2 : C.Hom B P}
ā Coprod.is-coproduct i1 i2 ā Co-prod.is-product i1 i2
is-coproductāis-co-product iscop =
record
{ āØ_,_ā©     = iscop.[_,_]
; Ļāāfactor = iscop.ināāfactor
; Ļāāfactor = iscop.ināāfactor
; unique    = iscop.unique
}
where module iscop = Coprod.is-coproduct iscop

## Co/equalisersš

import Cat.Diagram.Equaliser (C ^op) as Co-equ
import Cat.Diagram.Coequaliser C as Coequ

is-co-equaliserāis-coequaliser
: ā {A B E} {f g : C.Hom A B} {coeq : C.Hom B E}
ā Co-equ.is-equaliser f g coeq ā Coequ.is-coequaliser f g coeq
is-co-equaliserāis-coequaliser eq =
record
{ coequal    = eq.equal
; coequalise = eq.limiting
; universal  = eq.universal
; unique     = eq.unique
}
where module eq = Co-equ.is-equaliser eq

is-coequaliserāis-co-equaliser
: ā {A B E} {f g : C.Hom A B} {coeq : C.Hom B E}
ā Coequ.is-coequaliser f g coeq ā Co-equ.is-equaliser f g coeq
is-coequaliserāis-co-equaliser coeq =
record
{ equal     = coeq.coequal
; limiting  = coeq.coequalise
; universal = coeq.universal
; unique    = coeq.unique
}
where module coeq = Coequ.is-coequaliser coeq

## Initial/terminalš

import Cat.Diagram.Terminal (C ^op) as Coterm
import Cat.Diagram.Initial C as Init

is-initialāis-coterminal
: ā {A} ā Coterm.is-terminal A ā Init.is-initial A
is-initialāis-coterminal x = x

is-coterminalāis-initial
: ā {A} ā Init.is-initial A ā Coterm.is-terminal A
is-coterminalāis-initial x = x

## Pullback/pushoutš

import Cat.Diagram.Pullback (C ^op) as Co-pull
import Cat.Diagram.Pushout C as Push

is-co-pullbackāis-pushout
: ā {P X Y Z} {p1 : C.Hom X P} {f : C.Hom Z X} {p2 : C.Hom Y P} {g : C.Hom Z Y}
ā Co-pull.is-pullback p1 f p2 g ā Push.is-pushout f p1 g p2
is-co-pullbackāis-pushout pb =
record
{ square = pb.square
; colimiting = pb.limiting
; iāācolimiting = pb.pāālimiting
; iāācolimiting = pb.pāālimiting
; unique = pb.unique
}
where module pb = Co-pull.is-pullback pb

is-pushoutāis-co-pullback
: ā {P X Y Z} {p1 : C.Hom X P} {f : C.Hom Z X} {p2 : C.Hom Y P} {g : C.Hom Z Y}
ā Push.is-pushout f p1 g p2 ā Co-pull.is-pullback p1 f p2 g
is-pushoutāis-co-pullback po =
record
{ square      = po.square
; limiting    = po.colimiting
; pāālimiting = po.iāācolimiting
; pāālimiting = po.iāācolimiting
; unique      = po.unique
}
where module po = Push.is-pushout po

## Co/conesš

open import Cat.Diagram.Colimit.Base
open import Cat.Diagram.Limit.Base
open import Cat.Diagram.Terminal
open import Cat.Diagram.Initial

module _ {o ā} {J : Precategory o ā} {F : Functor J C} where
open Functor F renaming (op to F^op)

open Cocone-hom
open Cone-hom
open Terminal
open Initial
open Cocone
open Cone

Co-coneāCocone : Cone F^op ā Cocone F
Co-coneāCocone cone .coapex = cone .apex
Co-coneāCocone cone .Ļ = cone .Ļ
Co-coneāCocone cone .commutes = cone .commutes

CoconeāCo-cone : Cocone F ā Cone F^op
CoconeāCo-cone cone .apex     = cone .coapex
CoconeāCo-cone cone .Ļ        = cone .Ļ
CoconeāCo-cone cone .commutes = cone .commutes

CoconeāCo-coneāCocone : ā K ā Co-coneāCocone (CoconeāCo-cone K) ā” K
CoconeāCo-coneāCocone K i .coapex = K .coapex
CoconeāCo-coneāCocone K i .Ļ = K .Ļ
CoconeāCo-coneāCocone K i .commutes = K .commutes

Co-coneāCoconeāCo-cone : ā K ā CoconeāCo-cone (Co-coneāCocone K) ā” K
Co-coneāCoconeāCo-cone K i .apex = K .apex
Co-coneāCoconeāCo-cone K i .Ļ = K .Ļ
Co-coneāCoconeāCo-cone K i .commutes = K .commutes

Co-cone-homāCocone-hom
: ā {x y}
ā Cone-hom F^op y x
ā Cocone-hom F (Co-coneāCocone x) (Co-coneāCocone y)
Co-cone-homāCocone-hom ch .hom = ch .hom
Co-cone-homāCocone-hom ch .commutes o = ch .commutes o

Cocone-homāCo-cone-hom
: ā {x y}
ā Cocone-hom F x y
ā Cone-hom F^op (CoconeāCo-cone y) (CoconeāCo-cone x)
Cocone-homāCo-cone-hom ch .hom = ch .hom
Cocone-homāCo-cone-hom ch .commutes = ch .commutes

## Co/limitsš

ColimitāCo-limit
: Colimit F ā Limit F^op
ColimitāCo-limit colim = lim where
lim : Limit F^op
lim .top = CoconeāCo-cone (colim .bot)
lim .hasā¤ co-cone =
retractāis-contr f g fg
(colim .hasā„ (Co-coneāCocone co-cone))
where
f : _ ā _
f x = subst (Ī» e ā Cone-hom F^op e _)
(Co-coneāCoconeāCo-cone _)
(Cocone-homāCo-cone-hom x)

g : _ ā _
g x = subst (Ī» e ā Cocone-hom F e _)
(CoconeāCo-coneāCocone _)
(Co-cone-homāCocone-hom x)

fg : is-left-inverse f g
fg x = Cone-hom-path _ (transport-refl _ ā transport-refl _)

Co-limitāColimit
: Limit F^op ā Colimit F
Co-limitāColimit lim = colim where
colim : Colimit F
colim .bot = Co-coneāCocone (lim .top)
colim .hasā„ cocon =
retractāis-contr f g fg
(lim .hasā¤ (CoconeāCo-cone cocon))
where
f : _ ā _
f x = subst (Ī» e ā Cocone-hom F _ e)
(CoconeāCo-coneāCocone _)
(Co-cone-homāCocone-hom x)

g : _ ā _
g x = subst (Ī» e ā Cone-hom F^op _ e)
(Co-coneāCoconeāCo-cone _)
(Cocone-homāCo-cone-hom x)

fg : is-left-inverse f g
fg x = Cocone-hom-path _ (transport-refl _ ā transport-refl _)

module _ {o ā} {J : Precategory o ā} {F Fā² : Functor J C} where
private module JC = Cat.Reasoning Cat[ J , C ]

Colimit-ap-iso : F JC.ā Fā² ā Colimit F ā Colimit Fā²
Colimit-ap-iso f cl =
Co-limitāColimit (Limit-ap-iso (op-natural-iso f) (ColimitāCo-limit cl))