open import Cat.Prelude

open import Data.Sum

module Cat.Instances.Shape.Join where

Join of categoriesπŸ”—

The join C⋆D\mathcal{C} \star \mathcal{D} of two categories is the category obtained by β€œbridging” the disjoint union C∐D\mathcal{C} \coprod \mathcal{D} with a unique morphism between each object of C\mathcal{C} and each object of D\mathcal{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) = 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)