module Cat.Instances.Shape.Join where
Join of categoriesπ
The join of two categories is the category obtained by βbridgingβ the disjoint union with a unique morphism between each object of and each object of .
module _ {o β o' β'} (C : Precategory o β) (D : Precategory o' β') where private module C = Precategory C module D = Precategory D open Precategory βOb : Type (o β o') βOb = C.Ob β D.Ob βHom : (A B : βOb) β Type (β β β') βHom (inl x) (inl y) = Lift β' (C.Hom x y) βHom (inl x) (inr y) = Lift (β β β') β€ βHom (inr x) (inl y) = Lift (β β β') β₯ βHom (inr x) (inr y) = Lift β (D.Hom x y) βcompose : β {A B C : βOb} β βHom B C β βHom A B β βHom A C βcompose {inl x} {inl y} {inl z} (lift f) (lift g) = lift (f C.β g) βcompose {inl x} {inl y} {inr z} (lift f) (lift g) = lift tt βcompose {inl x} {inr y} {inr z} (lift f) (lift g) = lift tt βcompose {inr x} {inr y} {inr z} (lift f) (lift g) = lift (f D.β g) _β_ : Precategory _ _ _β_ .Ob = βOb _β_ .Hom = βHom _β_ .Hom-set x y = iss x y where iss : β x y β is-set (βHom x y) iss (inl x) (inl y) = hlevel! iss (inl x) (inr y) _ _ p q i j = lift tt iss (inr x) (inr y) = hlevel! _β_ .id {inl x} = lift C.id _β_ .id {inr x} = lift D.id _β_ ._β_ = βcompose _β_ .idr {inl x} {inl y} (lift f) = ap lift (C.idr f) _β_ .idr {inl x} {inr y} (lift f) = refl _β_ .idr {inr x} {inr y} (lift f) = ap lift (D.idr f) _β_ .idl {inl x} {inl y} (lift f) = ap lift (C.idl f) _β_ .idl {inl x} {inr y} (lift f) = refl _β_ .idl {inr x} {inr y} (lift f) = ap lift (D.idl f) _β_ .assoc {inl w} {inl x} {inl y} {inl z} (lift f) (lift g) (lift h) = ap lift (C.assoc f g h) _β_ .assoc {inl w} {inl x} {inl y} {inr z} (lift f) (lift g) (lift h) = refl _β_ .assoc {inl w} {inl x} {inr y} {inr z} (lift f) (lift g) (lift h) = refl _β_ .assoc {inl w} {inr x} {inr y} {inr z} (lift f) (lift g) (lift h) = refl _β_ .assoc {inr w} {inr x} {inr y} {inr z} (lift f) (lift g) (lift h) = ap lift (D.assoc f g h)