module Colimit where

open import Axioms public
open import InitialAlgebra public
open import Prelude public
open import ThinSemiCategory public

----------------------------------------------------------------------
-- Diagrams on thin semi categories
----------------------------------------------------------------------
record Diag (κ : Set){{_ : Thin κ}}(𝓒 : Set₁){{_ : CAT 𝓒}} : Set₁ where
  field
    V   : κ → 𝓒
    E   : ∀ i → ∏ᵇ j < i , (V j ⟶ V i)
    E∙E : ∀ i → ∀ᵇ j < i , ∀ᵇ k < j , (E i j ∙ E j k ≡ E i k)

open Diag public

----------------------------------------------------------------------
-- Categories with colimits of diagrams
----------------------------------------------------------------------
record Cocomplete (𝓒 : Set₁){{_ : CAT 𝓒}} : Set₁ where
  field
    colim : {κ : Set}{{_ : Thin κ}} → Diag κ 𝓒 → 𝓒
    inc :
      {κ : Set}
      {{_ : Thin κ}}
      (D : Diag κ 𝓒)
      (i : κ)
      → -------------
      V D i ⟶ colim D
    cocone :
      {κ : Set}
      {{_ : Thin κ}}
      (D : Diag κ 𝓒)
      {i : κ}
      → --------------------------------------
      ∀ᵇ j < i , (inc D j ≡ inc D i ∙ E D i j)
    lift :
      {κ : Set}
      {{_ : Thin κ}}
      (D : Diag κ 𝓒)
      {C : 𝓒}
      (f : ∀ i → V D i ⟶ C)
      (_ : {i : κ} → ∀ᵇ j < i , (f j ≡ f i ∙ E D i j))
      → ----------------------------------------------
      colim D ⟶ C
    liftinc :
      {κ : Set}
      {{_ : Thin κ}}
      (D : Diag κ 𝓒)
      {C : 𝓒}
      (f : ∀ i → V D i ⟶ C)
      (φ : ∀{i} → ∀ᵇ j < i , (f j ≡ f i ∙ E D i j))
      (i : κ)
      → -------------------------------------------
      f i ≡ lift D f φ ∙ inc D i
    liftuniq :
      {κ : Set}
      {{_ : Thin κ}}
      (D : Diag κ 𝓒)
      {C : 𝓒}
      (f : ∀ i → V D i ⟶ C)
      (φ : ∀{i} → ∀ᵇ j < i , (f j ≡ f i ∙ E D i j))
      {g : colim D ⟶ C}
      (_ : ∀ i → f i ≡ g ∙ inc D i)
      → -------------------------------------------
      lift D f φ ≡ g

  colimext :
    {κ : Set}
    {{_ : Thin κ}}
    (D : Diag κ 𝓒)
    {C : 𝓒}
    {f g : colim D ⟶ C}
    (_ : ∀ i → f ∙ inc D i ≡ g ∙ inc D i)
    → -----------------------------------
    f ≡ g
  colimext D {C} {f} {g} finc=ginc =
    proof
      f
    =[ symm (liftuniq D _ φ' (λ _ → refl)) ]
      lift D f' φ'
    =[ liftuniq D _ φ' finc=ginc ]
      g
    qed
    where
    f' : ∀ i → V D i ⟶ C
    f' i = f ∙ inc D i

    φ' : ∀{i} → ∀ᵇ j < i , (f' j ≡ f' i ∙ E D i j)
    φ' {i} j =
      proof
        f ∙ inc D j
      =[ ap (f ∙_) (cocone _ _) ]
        f ∙ (inc D i ∙ E D i j)
      =[ symm ∙assoc ]
        (f ∙ inc D i) ∙ E D i j
      qed

open Cocomplete {{...}} public

----------------------------------------------------------------------
-- Compose a functor with a diagram
----------------------------------------------------------------------
infix  _⊙_
_⊙_ :
  {𝓒 𝓓 : Set₁}
  {{_ : CAT 𝓒}}
  {{_ : CAT 𝓓}}
  (F : 𝓒 → 𝓓)
  {{_ : Functor F}}
  {κ : Set}
  {{_ : Thin κ}}
  (D : Diag κ 𝓒)
  → ---------------
  Diag κ 𝓓
V   (F ⊙ D) i = F (V D i)
E   (F ⊙ D) i j = F ′ (E D i j)
E∙E (_⊙_ F {{func}} D) i j k =
  proof
    F ′ (E D i j) ∙ F ′ (E D j k)
  =[ symm (act∙ {{r = func}}) ]
    F ′ (E D i j ∙ E D j k)
  =[ ap (F ′_) (E∙E D i j k) ]
     F ′ (E D i k)
  qed
-- The canonical morphism colim (F ⊙ D) → F (colim D)
can :
  {𝓒 𝓓 : Set₁}
  {{_ : CAT 𝓒}}
  {{_ : Cocomplete 𝓒}}
  {{_ : CAT 𝓓}}
  {{_ : Cocomplete 𝓓}}
  (F : 𝓒 → 𝓓)
  {{_ : Functor F}}
  {κ : Set}
  {{_ : Thin κ}}
  (D : Diag κ 𝓒)
  → -------------------------
  colim (F ⊙ D) ⟶ F (colim D)
can F {{func}} D = lift (F ⊙ D) caninc caninc'
  module _ where
  caninc : ∀ i →  F (V D i) ⟶ F (colim D)
  caninc i = F ′ inc D i

  caninc' : ∀{i} → ∀ᵇ j < i , (caninc j ≡ caninc i ∙ F ′ (E D i j))
  caninc' {i} j =
    proof
      F ′ (inc D j)
    =[ ap (F ′_) (cocone D j) ]
      F ′ (inc D i ∙ E D i j)
    =[ act∙ {{r = func}} ]
      F ′ (inc D i) ∙ F ′ (E D i j)
    qed

----------------------------------------------------------------------
-- Preservation of colimits
----------------------------------------------------------------------
Cocontinuous :
  (κ : Set)
  {{_ : Thin κ}}
  {𝓒 𝓓 : Set₁}
  {{_ : CAT 𝓒}}
  {{_ : CAT 𝓓}}
  {{_ : Cocomplete 𝓒}}
  {{_ : Cocomplete 𝓓}}
  (F : 𝓒 → 𝓓)
  {{_ : Functor F}}
  → ------------------
  Prop₁
Cocontinuous κ {𝓒} F = (D : Diag κ 𝓒) → Iso (can F D)

----------------------------------------------------------------------
-- Bounded diagrams on thin semi categories
----------------------------------------------------------------------
record Diagᵇ
  {κ : Set}
  {{_ : Thin κ}}
  (i : κ)
  (𝓒 : Set₁)
  {{_ : CAT 𝓒}}
  : -----------
  Set₁
  where
  field
    Vᵇ    : ∏ᵇ j < i , 𝓒
    Eᵇ    : ∏ᵇ j < i , ∏ᵇ k < j , (Vᵇ k ⟶ Vᵇ j)
    Eᵇ∙Eᵇ : ∀ᵇ j < i , ∀ᵇ k < j , ∀ᵇ l < k ,
      (Eᵇ j k ∙ Eᵇ k l ≡ Eᵇ j l)

open Diagᵇ public

-- Extensionality principle for Diagᵇ
Diagᵇext :
  {κ : Set}
  {{_ : Thin κ}}
  {𝓒 : Set₁}
  {{_ : CAT 𝓒}}
  {i : κ}
  {D D' : Diagᵇ i 𝓒}
  (_ : ∀ᵇ j < i , (Vᵇ D j ≡ Vᵇ D' j))
  (_ : ∀ᵇ j < i , ∀ᵇ k < j , (Eᵇ D j k ≣ Eᵇ D' j k))
  → ------------------------------------------------
  D ≡ D'
Diagᵇext {i = i} {D} {D'} v e =
  match VᵇD=VᵇD' \ where
    refl → match EᵇD=EᵇD' \ where
      refl → refl
  where
  VᵇD=VᵇD' : Vᵇ D ≡ Vᵇ D'
  VᵇD=VᵇD' = funext \
    j → instance-funexp \
      p → v j {{p}}

  EᵇD=EᵇD' : Eᵇ D ≣ Eᵇ D'
  EᵇD=EᵇD' = match VᵇD=VᵇD' \ where
    refl → funext \
      j → instance-funexp \
        p → funext \
          k → instance-funexp \
            q → e j {{p}} k {{q}}

-- Restriction of a bounded diagram
infixl  _⇂_
_⇂_ :
  {κ : Set}
  {{_ : Thin κ}}
  {𝓒 : Set₁}
  {{_ : CAT 𝓒}}
  (D : Diag κ 𝓒)
  (i : κ)
  → ------------
  Diagᵇ i 𝓒
Vᵇ    (D ⇂ _) j     = V D j
Eᵇ    (D ⇂ _) j k   = E D j k
Eᵇ∙Eᵇ (D ⇂ _) j k l = E∙E D j k l

infixl  _⇂ᵇ_
_⇂ᵇ_ :
  {κ : Set}
  {{_ : Thin κ}}
  {𝓒 : Set₁}
  {{_ : CAT 𝓒}}
  {i : κ}
  (D : Diagᵇ i 𝓒)
  (j : κ)
  {{_ : j <ᵇ i}}
  → -------------
  Diagᵇ j 𝓒
Vᵇ    (D ⇂ᵇ j)       = (Vᵇ D) ↓ᵇ j
Eᵇ    (D ⇂ᵇ j)       = (Eᵇ D) ↓ᵇ j
Eᵇ∙Eᵇ (D ⇂ᵇ j) k l m = Eᵇ∙Eᵇ D k l m

⇂ᵇ∙⇂ᵇ :
  {κ : Set}
  {{_ : Thin κ}}
  {𝓒 : Set₁}
  {{_ : CAT 𝓒}}
  {i : κ}
  (D : Diagᵇ i 𝓒)
  (j k : κ)
  {{_ : j <ᵇ i}}
  {{_ : k <ᵇ j}}
  → --------------------
  (D ⇂ᵇ j) ⇂ᵇ k ≡ D ⇂ᵇ k
⇂ᵇ∙⇂ᵇ D j k  = Diagᵇext (λ _ → refl) (λ _ _ → refl)

-- Compose an endofunctor with a bounded diagram
infix  _⊙ᵇ_
_⊙ᵇ_ :
  {𝓒 𝓓 : Set₁}
  {{_ : CAT 𝓒}}
  {{_ : CAT 𝓓}}
  (F : 𝓒 → 𝓓)
  {{_ : Functor F}}
  {κ : Set}
  {{_ : Thin κ}}
  {i : κ}
  → --------------------
  Diagᵇ i 𝓒 → Diagᵇ i 𝓓
Vᵇ (F ⊙ᵇ D) j   = F   (Vᵇ D j)
Eᵇ (F ⊙ᵇ D) j k = F ′ (Eᵇ D j k)
Eᵇ∙Eᵇ (_⊙ᵇ_ F {{func}} D) j k l =
  proof
    F ′ (Eᵇ D j k) ∙ F ′ (Eᵇ D k l)
  =[ symm (act∙ {{r = func}}) ]
    F ′ (Eᵇ D j k ∙ Eᵇ D k l)
  =[ ap (F ′_) (Eᵇ∙Eᵇ D j k l) ]
    F ′ (Eᵇ D j l)
  qed

----------------------------------------------------------------------
-- Colimit of a bounded diagram
----------------------------------------------------------------------
Dwn : (κ : Set){{_ : Thin κ}} → κ → Set
Dwn κ i = set j ∶ κ , (j < i)

dwn : {κ : Set}{{_ : Thin κ}}{i : κ} → ∏ᵇ j < i , Dwn κ i
dwn j {{p}} = j ∣ <prf p

instance
  ThinDwn :
    {κ : Set}
    {{_ : Thin κ}}
    {i : κ}
    → -----------
    Thin (Dwn κ i)
  _<_ {{ThinDwn}} k j = el k < el j
  <<  {{ThinDwn}} q p = << q p

diagᵇ :
  {κ : Set}
  {{_ : Thin κ}}
  {i : κ}
  {𝓒 : Set₁}
  {{_ : CAT 𝓒}}
  (D : Diagᵇ i 𝓒)
  → --------------
  Diag (Dwn κ i) 𝓒
V (diagᵇ D) j                               =
  Vᵇ D (el j) {{<inst (pf j)}}
E (diagᵇ D) j k {{<inst p}}                 =
  Eᵇ D (el j) {{<inst (pf j)}} (el k) {{<inst p}}
E∙E (diagᵇ D) j k {{<inst p}} l {{<inst q}} =
  Eᵇ∙Eᵇ D (el j) {{<inst (pf j)}} (el k) {{<inst p}} (el l) {{<inst q}}

colimᵇ :
  {κ : Set}
  {{_ : Thin κ}}
  (i : κ)
  {𝓒 : Set₁}
  {{_ : CAT 𝓒}}
  {{_ : Cocomplete 𝓒}}
  → ------------------
  Diagᵇ i 𝓒 → 𝓒
colimᵇ i D = colim (diagᵇ D)

incᵇ :
  {κ : Set}
  {{_ : Thin κ}}
  {i : κ}
  {𝓒 : Set₁}
  {{_ : CAT 𝓒}}
  {{_ : Cocomplete 𝓒}}
  (D : Diagᵇ i 𝓒)
  → ------------------------------
  ∏ᵇ j < i , (Vᵇ D j ⟶ colimᵇ i D)
incᵇ D j = inc (diagᵇ D) (dwn j)

coconeincᵇ :
  {κ : Set}
  {{_ : Thin κ}}
  {i : κ}
  {𝓒 : Set₁}
  {{_ : CAT 𝓒}}
  {{_ : Cocomplete 𝓒}}
  (D : Diagᵇ i 𝓒)
  → ----------------------------------------------------
  ∀ᵇ j < i , ∀ᵇ k < j , (incᵇ D k ≡ incᵇ D j ∙ Eᵇ D j k)
coconeincᵇ D j k {{p}} = cocone (diagᵇ D) (dwn k) {{<inst (<prf p)}}

module _
  {κ : Set}
  {{_ : Thin κ}}
  {i : κ}
  {𝓒 : Set₁}
  {{_ : CAT 𝓒}}
  {{_ : Cocomplete 𝓒}}
  (D : Diagᵇ i 𝓒)
  {C : 𝓒}
  (f : ∏ᵇ j < i , (Vᵇ D j ⟶ C))
  (φ : ∀ᵇ j < i , ∀ᵇ k < j , (f k ≡ f j ∙ Eᵇ D j k))
  where
  private
    f' : ((j ∣ p) : Dwn κ i) → (Vᵇ D j {{<inst p}} ⟶ C)
    f' (j ∣ p) = f j {{<inst p}}

    φ' : {j : Dwn κ i} → ∀ᵇ k < j , (f' k ≡ f' j ∙ E (diagᵇ D) j k )
    φ' {j ∣ p} (k ∣ _) {{<inst r}} = φ j {{<inst p}} k {{<inst r}}

  liftᵇ : colimᵇ i D ⟶ C
  liftᵇ = lift (diagᵇ D) f' φ'

  liftincᵇ : ∀ᵇ j < i , (f j ≡ liftᵇ ∙ incᵇ D j)
  liftincᵇ j = liftinc (diagᵇ D) f' φ' (dwn j)

  liftuniqᵇ :
    (g : colimᵇ i D ⟶ C)
    (ψ : ∀ᵇ j < i , (f j ≡ g ∙ incᵇ D j))
    → -----------------------------------
    liftᵇ ≡ g
  liftuniqᵇ g ψ =
    liftuniq (diagᵇ D) f' φ' {g} λ{(j ∣ p) → ψ j {{<inst p}}}

colimextᵇ :
  {κ : Set}
  {{_ : Thin κ}}
  {i : κ}
  {𝓒 : Set₁}
  {{_ : CAT 𝓒}}
  {{_ : Cocomplete 𝓒}}
  (D : Diagᵇ i 𝓒)
  {C : 𝓒}
  {f g : colimᵇ i D ⟶ C}
  (_ : ∀ᵇ j < i , (f ∙ incᵇ D j ≡ g ∙ incᵇ D j))
  → --------------------------------------------
  f ≡ g
colimextᵇ {κ} {i} D e = colimext (diagᵇ D) λ{(j ∣ p) → e j {{<inst p}}}

colimᵇ⇂ :
  {κ : Set}
  {{_ : Thin κ}}
  (i j : κ)
  {{_ : j <ᵇ i}}
  {𝓒 : Set₁}
  {{_ : CAT 𝓒}}
  {{_ : Cocomplete 𝓒}}
  (D : Diagᵇ i 𝓒)
  → ----------------------------
  colimᵇ j (D ⇂ᵇ j) ⟶ colimᵇ i D
colimᵇ⇂ i j D = liftᵇ (D ⇂ᵇ j)
  (λ k   → incᵇ D k)
  (λ k l → coconeincᵇ D k l)

colimᵇ⇂incᵇ :
  {κ : Set}
  {{_ : Thin κ}}
  (i j k : κ)
  {{_ : j <ᵇ i}}
  {{_ : k <ᵇ j}}
  {𝓒 : Set₁}
  {{_ : CAT 𝓒}}
  {{_ : Cocomplete 𝓒}}
  (D : Diagᵇ i 𝓒)
  → ----------------------------------------
  incᵇ D k ≡ colimᵇ⇂ i j D ∙ incᵇ (D ⇂ᵇ j) k
colimᵇ⇂incᵇ i j k D = liftincᵇ (D ⇂ᵇ j)
  (λ k   → incᵇ D k)
  (λ k l → coconeincᵇ D k l) k