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
: Type (o β o')
βOb = C.Ob β D.Ob
βOb
: (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)
βHom
: β {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)
βcompose
_β_ : Precategory _ _
_β_ .Ob = βOb
_β_ .Hom = βHom
_β_ .Hom-set x y = iss x y where
: β x y β is-set (βHom x y)
iss (inl x) (inl y) = hlevel 2
iss (inl x) (inr y) _ _ p q i j = lift tt
iss (inr x) (inr y) = hlevel 2
iss _β_ .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)
module _ {o β o' β'} {C : Precategory o β} {D : Precategory o' β'} where
: Functor C (C β D)
β-inl .Fβ = inl
β-inl .Fβ = lift
β-inl .F-id = refl
β-inl .F-β f g = refl
β-inl
: Functor D (C β D)
β-inr .Fβ = inr
β-inr .Fβ = lift
β-inr .F-id = refl
β-inr .F-β f g = refl
β-inr
module _ {oc βc od βd oe βe}
{C : Precategory oc βc} {D : Precategory od βd} {E : Precategory oe βe}
where
: Functor C D β Functor (C β E) (D β E)
β-mapl .Fβ = β-mapl (F .Fβ)
β-mapl F .Fβ {inl x} {inl y} (lift f) = lift (F .Fβ f)
β-mapl F .Fβ {inl x} {inr y} _ = _
β-mapl F .Fβ {inr x} {inr y} (lift f) = lift f
β-mapl F .F-id {inl x} = ap lift (F .F-id)
β-mapl F .F-id {inr x} = refl
β-mapl F .F-β {inl x} {inl y} {inl z} f g = ap lift (F .F-β _ _)
β-mapl F .F-β {inl x} {inl y} {inr z} f g = refl
β-mapl F .F-β {inl x} {inr y} {inr z} f g = refl
β-mapl F .F-β {inr x} {inr y} {inr z} f g = refl
β-mapl F
: Functor D E β Functor (C β D) (C β E)
β-mapr .Fβ = β-mapr (F .Fβ)
β-mapr F .Fβ {inl x} {inl y} (lift f) = lift f
β-mapr F .Fβ {inl x} {inr y} _ = _
β-mapr F .Fβ {inr x} {inr y} (lift f) = lift (F .Fβ f)
β-mapr F .F-id {inl x} = refl
β-mapr F .F-id {inr x} = ap lift (F .F-id)
β-mapr F .F-β {inl x} {inl y} {inl z} f g = refl
β-mapr F .F-β {inl x} {inl y} {inr z} f g = refl
β-mapr F .F-β {inl x} {inr y} {inr z} f g = refl
β-mapr F .F-β {inr x} {inr y} {inr z} f g = ap lift (F .F-β _ _) β-mapr F
Adjoining a terminal objectπ
Given a category we can freely adjoin a terminal object to by taking the join with the terminal category.
_βΉ : β {o β} β Precategory o β β Precategory o β
= J β β€Cat
J βΉ
module _ {o β} {J : Precategory o β} where
: Functor J (J βΉ)
βΉ-in = β-inl
βΉ-in
: Functor (J βΉ βΉ) (J βΉ)
βΉ-join .Fβ (inl (inl j)) = inl j
βΉ-join .Fβ (inl (inr _)) = inr _
βΉ-join .Fβ (inr _) = inr _
βΉ-join .Fβ {inl (inl x)} {inl (inl y)} (lift f) = f
βΉ-join .Fβ {inl (inl x)} {inl (inr y)} f = _
βΉ-join .Fβ {inl (inl x)} {inr y} f = _
βΉ-join .Fβ {inl (inr x)} {inl (inr y)} f = _
βΉ-join .Fβ {inl (inr x)} {inr y} f = _
βΉ-join .Fβ {inr x} {inr y} f = _
βΉ-join .F-id {inl (inl x)} = refl
βΉ-join .F-id {inl (inr x)} = refl
βΉ-join .F-id {inr x} = refl
βΉ-join .F-β {inl (inl x)} {inl (inl y)} {inl (inl z)} f g = refl
βΉ-join .F-β {inl (inl x)} {inl (inl y)} {inl (inr z)} f g = refl
βΉ-join .F-β {inl (inl x)} {inl (inl y)} {inr z} f g = refl
βΉ-join .F-β {inl (inl x)} {inl (inr y)} {inl (inr z)} f g = refl
βΉ-join .F-β {inl (inl x)} {inl (inr y)} {inr z} f g = refl
βΉ-join .F-β {inl (inl x)} {inr y} {inr z} f g = refl
βΉ-join .F-β {inl (inr x)} {inl (inr y)} {inl (inr z)} f g = refl
βΉ-join .F-β {inl (inr x)} {inl (inr y)} {inr z} f g = refl
βΉ-join .F-β {inl (inr x)} {inr y} {inr z} f g = refl
βΉ-join .F-β {inr x} {inr y} {inr z} f g = refl βΉ-join