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 is the other in . 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))