open import Cat.Instances.Shape.Terminal
open import Cat.Prelude

open import Data.Sum

open Precategory
open Functor

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

  ⋆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 2
    iss (inl x) (inr y) _ _ p q i j = lift tt
    iss (inr x) (inr y) = hlevel 2
  _⋆_ .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
  ⋆-inl : Functor C (C ⋆ D)
  ⋆-inl .Fβ‚€ = inl
  ⋆-inl .F₁ = lift
  ⋆-inl .F-id = refl
  ⋆-inl .F-∘ f g = refl

  ⋆-inr : Functor D (C ⋆ D)
  ⋆-inr .Fβ‚€ = inr
  ⋆-inr .F₁ = lift
  ⋆-inr .F-id = refl
  ⋆-inr .F-∘ f g = refl

module _ {oc β„“c od β„“d oe β„“e}
  {C : Precategory oc β„“c} {D : Precategory od β„“d} {E : Precategory oe β„“e}
  where

  ⋆-mapl : Functor C D β†’ Functor (C ⋆ E) (D ⋆ E)
  ⋆-mapl F .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

  ⋆-mapr : Functor D E β†’ Functor (C ⋆ D) (C ⋆ E)
  ⋆-mapr F .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-∘ _ _)

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 β–Ή = J ⋆ ⊀Cat

module _ {o β„“} {J : Precategory o β„“} where
  β–Ή-in : Functor J (J β–Ή)
  β–Ή-in = ⋆-inl

  β–Ή-join : 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