open import Cat.Prelude

open import Data.Sum

module Cat.Instances.Shape.Join where


Join of categoriesπ

The join $\ca{C} \star \ca{D}$ of two categories is the category obtained by βbridgingβ the disjoint union $\ca{C} \coprod \ca{D}$ with a unique morphism between each object of $\ca{C}$ and each object of $\ca{D}$.

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) = Lift-is-hlevel 2 (C.Hom-set x y)
iss (inl x) (inr y) _ _ p q i j = lift tt
iss (inr x) (inr y) = Lift-is-hlevel 2 (D.Hom-set x y)
_β_ .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)