module InitialAlgebraViaInflationaryIteration where

open import Axioms public
open import Colimit public
open import InflationaryIteration public
open import InitialAlgebra public
open import Prelude public
open import Size public
open import ThinSemiCategory public
open import WellFoundedRelations public

----------------------------------------------------------------------
-- Properties of the size-indexed inflationary iteration of F
----------------------------------------------------------------------
module InflProp
  {𝓒 : Set₁}
  {{_ : CAT 𝓒}}
  {{_ : Cocomplete 𝓒}}
  (F : 𝓒 → 𝓒)
  {{_ : Functor F}}
  (κ : Set)
  {{_ : Size κ}}
  (D : Diag κ 𝓒)
  (InflFκD : Infl F κ D)
  where
  τ : ∀ i → ∏ᵇ j < i , (F (V D j) ⟶ V D i)
  τ i j =
    subst (F (V D j) ⟶_) (symm (∧e₁ (InflFκD i)))
    (incᵇ (F ⊙ᵇ (D ⇂ i)) j)

  Eτ : ∀ i → ∀ᵇ j < i , ∀ᵇ k < j , (τ i k ≡ E D i j ∙ τ j k)
  Eτ i j k = triangleq (τ j k) (E D i j) (τ i k)
    refl
    (∧e₁ (InflFκD j))
    (∧e₁ (InflFκD i))
    (incᵇ (F ⊙ᵇ (D ⇂ j)) k)
    (colimᵇ⇂ i j (F ⊙ᵇ (D ⇂ i)))
    (incᵇ (F ⊙ᵇ (D ⇂ i)) k)
    (subst≣ (F (V D k) ⟶_) (symm (∧e₁ (InflFκD j))) _)
    (∧e₂ (InflFκD i) j)
    (subst≣ (F (V D k) ⟶_) (symm (∧e₁ (InflFκD i))) _)
    (liftincᵇ (F ⊙ᵇ (D ⇂ j))
      (λ k → incᵇ (F ⊙ᵇ (D ⇂ i)) k)
      (λ k l → coconeincᵇ (F ⊙ᵇ (D ⇂ i)) k l) k)

  τE : ∀ i → ∀ᵇ j < i , ∀ᵇ k < j , (τ i k ≡ τ i j ∙ F ′ E D j k)
  τE i j k = triangleq (F ′ E D j k) (τ i j) (τ i k)
    refl
    refl
    (∧e₁ (InflFκD i))
    (F ′ E D j k)
    (incᵇ (F ⊙ᵇ (D ⇂ i)) j)
    (incᵇ (F ⊙ᵇ (D ⇂ i)) k)
    refl
    (subst≣ (F (V D j) ⟶_) (symm (∧e₁ (InflFκD i))) _)
    (subst≣ (F (V D k) ⟶_) (symm (∧e₁ (InflFκD i))) _)
    (coconeincᵇ (F ⊙ᵇ (D ⇂ i)) j k)

  τext :
    (i : κ)
    {X : 𝓒}
    {f g : V D i ⟶ X}
    (_ : ∀ᵇ j < i , (f ∙ τ i j ≡ g ∙ τ i j))
    → ---------------------------------------
    f ≡ g
  τext i {X} {f} {g} e =
    proof
      f
    =[ f=f' ]
      f'
    =[ f'=g' ]
      g'
    =[ g'=g ]
      g
    qed
    where
    f' : colimᵇ i (F ⊙ᵇ (D ⇂ i)) ⟶ X
    f' = subst (_⟶ X) (∧e₁ (InflFκD i)) f

    f=f' : f ≣ f'
    f=f' = symm (subst≣ (_⟶ X) (∧e₁ (InflFκD i)) f)

    f'incᵇ=fτ : ∀ᵇ j < i ,
      (f' ∙ incᵇ (F ⊙ᵇ (D ⇂ i)) j ≡ f ∙ τ i j)
    f'incᵇ=fτ j = triangleq (τ i j) f (f' ∙ incᵇ (F ⊙ᵇ (D ⇂ i)) j)
      refl
      (∧e₁ (InflFκD i))
      refl
      (incᵇ (F ⊙ᵇ (D ⇂ i)) j)
      f'
      (f' ∙ incᵇ (F ⊙ᵇ (D ⇂ i)) j)
      (subst≣ (F (V D j) ⟶_) (symm (∧e₁ (InflFκD i))) _)
      f=f'
      refl
      refl

    g' : colimᵇ i (F ⊙ᵇ (D ⇂ i)) ⟶ X
    g' = subst (_⟶ X) (∧e₁ (InflFκD i)) g

    g'=g : g' ≣ g
    g'=g = subst≣ (_⟶ X) (∧e₁ (InflFκD i)) g

    gτ=g'incᵇ : ∀ᵇ j < i ,
      (g ∙ τ i j ≡ g' ∙ incᵇ (F ⊙ᵇ (D ⇂ i)) j)
    gτ=g'incᵇ j = triangleq (incᵇ (F ⊙ᵇ (D ⇂ i)) j) g' (g ∙ τ i j)
      refl
      (symm (∧e₁ (InflFκD i)))
      refl
      (τ i j) g
      (g ∙ τ i j)
      (symm (subst≣ (F (V D j) ⟶_) (symm (∧e₁ (InflFκD i))) _))
      g'=g
      refl
      refl

    f'=g' : f' ≡ g'
    f'=g' = colimextᵇ (F ⊙ᵇ (D ⇂ i)) λ j →
      proof
        f' ∙ incᵇ (F ⊙ᵇ (D ⇂ i)) j
      =[ f'incᵇ=fτ j ]
        f ∙ τ i j
      =[ e j ]
        g ∙ τ i j
      =[ gτ=g'incᵇ j ]
        g' ∙ incᵇ (F ⊙ᵇ (D ⇂ i)) j
      qed

----------------------------------------------------------------------
-- If an endofunctor F on a cocomplete category preserves κ-indexed
-- colimits for some size κ, then any κ-indexed inflationary iteration
-- of F yields an initial F-algebra
----------------------------------------------------------------------
Cocontinuous∧Inflationary→Initial :
  (κ : Set)
  {{_ : Size κ}}
  {𝓒 : Set₁}
  {{_ : CAT 𝓒}}
  {{_ : Cocomplete 𝓒}}
  (F : 𝓒 → 𝓒)
  {{_ : Functor F}}
  (_ : Cocontinuous κ F)
  (D : Diag κ 𝓒)
  (InflFκD : Infl F κ D)
  → ---------------------
  InitialAlg F
Cocontinuous∧Inflationary→Initial κ {𝓒} F coconκF D InflFκD =
  record
    { obj = obj
    ; alg = alg
    ; fun = fun
    ; hom = hom
    ; unq = unq
    }
  where
  open InflProp F κ D InflFκD

  -- The inital F-algebra
  obj : 𝓒
  obj = colim D

  instance
    _ : Iso (can F D)
    _ = coconκF D

    alg : Alg F obj
    fold {{alg}} = lift (F ⊙ D) foldᵇ coconefoldᵇ ∙ (can F D)⁻¹
      module _ where
        foldᵇ : ∀ i → F (V D i) ⟶ obj
        foldᵇ i = inc D (↑ˢ i) ∙ τ (↑ˢ i) i {{<ᵇ↑ˢ}}

        coconefoldᵇ : ∀{i} → ∀ᵇ j < i ,
          (foldᵇ j ≡ foldᵇ i ∙ F ′ (E D i j))
        coconefoldᵇ {i} j =
          let
            i' = ↑ˢ i
            j' = ↑ˢ j
            k = i' ⊔ˢ j'
            instance
              _ : i <ᵇ i'
              _ = <ᵇ↑ˢ
              _ : j <ᵇ j'
              _ = <ᵇ↑ˢ
              _ : i' <ᵇ k
              _ = <ᵇ⊔ˢl
              _ : j' <ᵇ k
              _ = <ᵇ⊔ˢr
          in
            proof
              inc D j' ∙ τ j' j
            =[ ap (_∙ τ j' j) (cocone D j') ]
              (inc D k ∙ E D k j') ∙ τ j' j
            =[ ∙assoc ]
              inc D k ∙ (E D k j' ∙ τ j' j)
            =[ ap (inc D k ∙_) (symm (Eτ k j' j)) ]
              inc D k ∙ τ k j
            =[ ap (inc D k ∙_) (Eτ k i' j) ]
              inc D k ∙ (E D k i' ∙ τ i' j)
            =[ symm ∙assoc ]
              (inc D k ∙ E D k i') ∙ τ i' j
            =[ ap (_∙ τ i' j) (symm (cocone D i')) ]
              inc D i' ∙ τ i' j
            =[ ap (inc D i' ∙_) (τE i' i j) ]
              inc D i' ∙ (τ i' i ∙ F ′ E D i j)
            =[ symm ∙assoc ]
              (inc D i' ∙ τ i' i) ∙ F ′ E D i j
            qed

  -- Existence part of the universal property of the initial F-algebra
  module _ (A : 𝓒){{_ : Alg F A}}
    where
    -- Size-bounded morphism to A
    Homᵇ : (i : κ) → (V D i ⟶ A) → Prop
    Homᵇ i h = ∀ᵇ j < i , (h ∙ τ i j ≡ fold ∙ F ′ (h ∙ E D i j))

    -- Size-bounded morphisms restrict
    Homᵇ⇂ :
      {i : κ}
      (h : V D i ⟶ A)
      → ----------------------------------------
      Homᵇ i h → ∀ᵇ j < i , Homᵇ j (h ∙ E D i j)
    Homᵇ⇂ {i} h φ j k =
      proof
        (h ∙ E D i j) ∙ τ j k
      =[ ∙assoc ]
        h ∙ (E D i j ∙ τ j k)
      =[ ap (h ∙_) (symm (Eτ i j k)) ]
        h ∙ τ i k
      =[ φ k ]
        fold ∙ F ′ (h ∙ E D i k)
      =[ ap (λ g → fold ∙ F ′ (h ∙ g)) (symm (E∙E D i j k)) ]
        fold ∙ F ′ (h ∙ (E D i j ∙ E D j k))
      =[ ap (λ f → fold ∙ F ′ f) (symm ∙assoc) ]
        fold ∙ F ′ ((h ∙ E D i j) ∙ E D j k)
      qed

    -- Size-bounded morphisms are unique
    Homᵇuniq :
      (i : κ)
      (h h' : V D i ⟶ A)
      → ----------------------------
      Homᵇ i h → Homᵇ i h' → h ≡ h'
    Homᵇuniq = <ind P hyp
      where
      P : κ → Prop
      P i = ∀ h h' → Homᵇ i h → Homᵇ i h' → h ≡ h'

      hyp : ∀ i → (∀ᵇ j < i , P j) → P i
      hyp i hi h h' φ φ' = τext i λ j →
        proof
          h ∙ τ i j
        =[ φ j ]
          fold ∙ F ′ (h ∙ E D i j)
        =[ ap (λ f → fold ∙ F ′ f)
           ((hi j (h ∙ E D i j) (h' ∙ E D i j)
           (Homᵇ⇂ h φ j) (Homᵇ⇂ h' φ' j))) ]
          fold ∙ F ′ (h' ∙ E D i j)
        =[ symm (φ' j) ]
          h' ∙ τ i j
        qed

    -- Size-bounded morphisms exist
    Hom : κ → Set
    Hom i = set (V D i ⟶ A) (Homᵇ i)

    hyp : ∀ i → (∏ᵇ j < i , Hom j) → Hom i
    hyp i hi = h ∣ Homᵇh
      where
      hᵇ : ∏ᵇ j < i , (F (V D j) ⟶ A)
      hᵇ j = fold ∙ F ′ el (hi j)

      coconehᵇ : ∀ᵇ j < i , ∀ᵇ k < j ,
        (hᵇ k ≡ hᵇ j ∙ F ′ E D j k)
      coconehᵇ j k =
        proof
          fold ∙ F ′ el (hi k)
        =[ ap (λ g → fold ∙ F ′ g)
           (Homᵇuniq k (el (hi k)) (el (hi j) ∙ E D j k)
           (pf (hi k)) (Homᵇ⇂ (el (hi j)) (pf (hi j)) k )) ]
          fold ∙ F ′ (el (hi j) ∙ E D j k)
        =[ ap (fold ∙_) act∙ ]
          fold ∙ (F ′ el (hi j) ∙ F ′ E D j k)
        =[ symm ∙assoc ]
          (fold ∙ F ′ el (hi j)) ∙ F ′ E D j k
        qed

      h : V D i ⟶ A
      h =
        subst (_⟶ A) (symm (∧e₁ (InflFκD i)))
        (liftᵇ (F ⊙ᵇ (D ⇂ i)) hᵇ coconehᵇ)


      hτ : ∀ᵇ j < i , (hᵇ j ≡ h ∙ τ i j)
      hτ j = triangleq (τ i j) h (hᵇ j)
        refl
        (∧e₁ (InflFκD i))
        refl
        (incᵇ (F ⊙ᵇ (D ⇂ i)) j)
        ((liftᵇ (F ⊙ᵇ (D ⇂ i)) hᵇ coconehᵇ))
        (hᵇ j)
        (subst≣ (F (V D j) ⟶_) (symm (∧e₁ (InflFκD i))) _)
        (subst≣ (_⟶ A) (symm (∧e₁ (InflFκD i))) _)
        refl
        (liftincᵇ (F ⊙ᵇ (D ⇂ i)) hᵇ coconehᵇ j)

      h⇂ : ∀ᵇ j < i , (h ∙ E D i j ≡ el (hi j))
      h⇂ j = τext j (λ k →
        proof
          (h ∙ E D i j) ∙ τ j k
        =[ ∙assoc ]
          h ∙ (E D i j ∙ τ j k)
        =[ ap (h ∙_) (symm (Eτ i j k)) ]
          h ∙ τ i k
        =[ symm (hτ k) ]
          fold ∙ F ′ el (hi k)
        =[ ap (λ g → fold ∙ F ′ g)
           (((Homᵇuniq k (el (hi k)) (el (hi j) ∙ E D j k)
           (pf (hi k)) (Homᵇ⇂ (el (hi j)) (pf (hi j)) k )))) ]
          fold ∙ F ′ (el (hi j) ∙ E D j k)
        =[ symm (pf (hi j) k) ]
          el (hi j) ∙ τ j k
        qed)

      Homᵇh : Homᵇ i h
      Homᵇh j =
        proof
          h ∙ τ i j
        =[ symm (hτ j) ]
          fold ∙ F ′ el (hi j)
        =[ ap (λ g → fold ∙ F ′ g) (symm (h⇂ j)) ]
          fold ∙ F ′ (h ∙ E D i j)
        qed

    -- The cone whose colimit is the uniqe F-algebra morphism obj → A
    f : ∀ i → V D i ⟶ A
    f i = el (<rec Hom hyp i)

    Homᵇf : ∀ i → Homᵇ i (f i)
    Homᵇf i = pf (<rec Hom hyp i)

    coconef : ∀{i} → ∀ᵇ j < i , (f j ≡ f i ∙ E D i j)
    coconef {i} j =
      Homᵇuniq j (f j) (f i ∙ E D i j )
      (Homᵇf j) (Homᵇ⇂ (f i) (Homᵇf i) j)

    fτ : ∀ i → ∀ᵇ j < i , (f i ∙ τ i j ≡ fold ∙ F ′ f j)
    fτ i j =
      proof
        f i ∙ τ i j
      =[ Homᵇf i j ]
        fold ∙ F ′ (f i ∙ E D i j)
      =[ ap (λ f₁ → fold ∙ F ′ f₁)
         (Homᵇuniq j (f i ∙ E D i j) (f j)
         (Homᵇ⇂ (f i) (Homᵇf i) j) (Homᵇf j)) ]
        fold ∙ F ′ f j
      qed

    -- The unique F-algebra morphism obj → A
    fun : obj ⟶ A
    fun = lift D f coconef

    hom : AlgHom F fun
    hom =
      proof
        -- fun ∙ fold
        fun ∙ (lift (F ⊙ D) foldᵇ coconefoldᵇ ∙ (can F D)⁻¹)
      =[ symm ∙assoc ]
        (fun ∙ lift (F ⊙ D) foldᵇ coconefoldᵇ) ∙ (can F D)⁻¹
      =[  ap (_∙ (can F D ⁻¹)) e ]
        ((fold ∙ F ′ fun) ∙ can F D) ∙ (can F D)⁻¹
      =[ ∙assoc ]
        (fold ∙ F ′ fun) ∙ (can F D ∙ (can F D)⁻¹)
      =[ ap ((fold ∙ F ′ fun) ∙_) (rinv _) ]
        (fold ∙ F ′ fun) ∙ ide _
      =[ ∙ide ]
        fold ∙ F ′ fun
      qed
      where
      e : fun ∙ lift (F ⊙ D) foldᵇ coconefoldᵇ ≡
          (fold ∙ F ′ fun) ∙ can F D
      e = colimext (F ⊙ D) λ i →
        proof
          (fun ∙ lift (F ⊙ D) foldᵇ coconefoldᵇ) ∙ inc (F ⊙ D) i
        =[ ∙assoc ]
          fun ∙ (lift (F ⊙ D) foldᵇ coconefoldᵇ ∙ inc (F ⊙ D) i)
        =[ ap (fun ∙_) (symm (liftinc (F ⊙ D) _ coconefoldᵇ _)) ]
          fun ∙ (inc D (↑ˢ i) ∙ τ (↑ˢ i) i {{<ᵇ↑ˢ}})
        =[ symm ∙assoc ]
          (fun ∙ inc D (↑ˢ i)) ∙ τ (↑ˢ i) i {{<ᵇ↑ˢ}}
        =[ ap (_∙ τ (↑ˢ i) i {{<ᵇ↑ˢ}})
           (symm (liftinc D _ coconef _)) ]
          f (↑ˢ i) ∙ τ (↑ˢ i) i {{<ᵇ↑ˢ}}
        =[ fτ (↑ˢ i) i {{<ᵇ↑ˢ}} ]
          fold ∙ F ′ f i
        =[ ap (λ g → fold ∙ F ′ g) (liftinc D _ coconef _) ]
          fold ∙ F ′ (fun ∙ inc D i)
        =[ ap (fold ∙_) act∙ ]
          fold ∙ (F ′ fun ∙ F ′ inc D i)
        =[ symm ∙assoc ]
          (fold ∙ F ′ fun) ∙ F ′ inc D i
        =[ ap ((fold ∙ F ′ fun) ∙_)
           (liftinc (F ⊙ D) _ (caninc' F D) _) ]
          (fold ∙ F ′ fun) ∙ (can F D ∙ inc (F ⊙ D) i)
        =[ symm ∙assoc ]
          ((fold ∙ F ′ fun) ∙ can F D) ∙ inc (F ⊙ D) i
        qed
    abstract
      Uniqᵇ :
        (g : obj ⟶ A)
        (_ : AlgHom F g)
        (i j : κ)
        {{_ : j <ᵇ i}}
        → -----------------------------------------------
        fold ∙ F ′ (g ∙ inc D j) ≡ (g ∙ inc D i) ∙ τ i j
      Uniqᵇ g AlgHomg i j =
        let
          j' = ↑ˢ j
          k = i ⊔ˢ j'
          instance
            _ : i <ᵇ k
            _ = <ᵇ⊔ˢl
            _ : j <ᵇ j'
            _ = <ᵇ↑ˢ
            _ : j' <ᵇ k
            _ = <ᵇ⊔ˢr
        in
        proof
          fold ∙ F ′ (g ∙ inc D j)
        =[ ap (fold ∙_) act∙ ]
          fold ∙ (F ′ g ∙ F ′ inc D j)
        =[ symm ∙assoc ]
          (fold ∙ F ′ g) ∙ F ′ inc D j
        =[ ap (_∙ F ′ inc D j) (symm AlgHomg) ]
          (g ∙ fold {A = obj}) ∙ F ′ inc D j
        =[ ap ((g ∙ fold {A = obj}) ∙_)
          (liftinc (F ⊙ D) _ (caninc' F D) _) ]
          (g ∙ fold {A = obj}) ∙ (can F D ∙ inc (F ⊙ D) j)
        =[ symm ∙assoc ]
          ((g ∙ fold {A = obj}) ∙ can F D) ∙ inc (F ⊙ D) j
        =[ ap (_∙ inc (F ⊙ D) j) ∙assoc ]
          (g ∙ (fold {A = obj} ∙ can F D)) ∙ inc (F ⊙ D) j
        =[ ap (λ h → (g ∙ h) ∙ inc  (F ⊙ D) j) ∙assoc ]
          (g ∙ (lift (F ⊙ D) foldᵇ coconefoldᵇ ∙
            ((can F D)⁻¹ ∙ can F D))) ∙ inc (F ⊙ D) j
        =[ ap (λ h → (g ∙ lift (F ⊙ D) foldᵇ coconefoldᵇ ∙ h) ∙ inc (F ⊙ D) j)
           (linv _) ]
          (g ∙ (lift (F ⊙ D) foldᵇ coconefoldᵇ ∙ ide _)) ∙ inc (F ⊙ D) j
        =[ ap (λ h → (g ∙ h) ∙ inc (F ⊙ D) j) ∙ide ]
          (g ∙ lift (F ⊙ D) foldᵇ coconefoldᵇ) ∙ inc (F ⊙ D) j
        =[ ∙assoc ]
          g ∙ (lift (F ⊙ D) foldᵇ coconefoldᵇ ∙ inc (F ⊙ D) j)
        =[ ap (g ∙_) (symm (liftinc (F ⊙ D) _ coconefoldᵇ _)) ]
          g ∙ (inc D j' ∙ τ j' j)
        =[ ap (λ h → g ∙ h ∙ τ j' j) (cocone D j') ]
          g ∙ ((inc D k ∙ E D k j') ∙ τ j' j)
        =[ ap (g ∙_) ∙assoc ]
          g ∙ (inc D k ∙ (E D k j' ∙ τ j' j))
        =[ ap (λ h → g ∙ inc D k ∙ h) (symm (Eτ k j' j)) ]
          g ∙ (inc D k ∙ τ k j)
        =[ ap (λ h → g ∙ inc D k ∙ h) (Eτ k i j) ]
          g ∙ (inc D k ∙ (E D k i ∙ τ i j))
        =[ ap (g ∙_) (symm ∙assoc)  ]
          g ∙ ((inc D k ∙ E D k i) ∙ τ i j)
        =[ symm ∙assoc ]
          (g ∙ (inc D k ∙ E D k i)) ∙ τ i j
        =[ ap (λ h → (g ∙ h) ∙ τ i j) (symm (cocone D i)) ]
          (g ∙ inc D i) ∙ τ i j
        qed

      unq : {g : obj ⟶ A} → AlgHom F g → fun ≡ g
      unq {g} AlgHomg = colimext D (<ind P p)
        where
        P : κ → Prop
        P i = fun ∙ inc _ i ≡ g ∙ inc _ i

        p : ∀ i → (∀ᵇ j < i , P j) → P i
        p i pi = τext i λ j →
          proof
            (fun ∙ inc _ i) ∙ τ i j
          =[ symm (Uniqᵇ fun hom i j) ]
            fold ∙ F ′ (fun ∙ inc _ j)
          =[ ap (λ f₁ → fold ∙ F ′ f₁) (pi j) ]
            fold ∙ F ′ (g ∙ inc _ j)
          =[ Uniqᵇ g AlgHomg i j ]
            (g ∙ inc _ i) ∙ τ i j
          qed

----------------------------------------------------------------------
-- Theorem 3.8: any endofunctor F on a cocomplete category which
-- preserves κ-indexed colimits for some size κ has an initial algebra
----------------------------------------------------------------------
InitialAlgebraTheorem :
  (κ : Set)
  {{s : Size κ}}
  {𝓒 : Set₁}
  {{_ : CAT 𝓒}}
  {{_ : Cocomplete 𝓒}}
  (F : 𝓒 → 𝓒)
  {{_ : Functor F}}
  (_ : Cocontinuous κ F)
  → --------------------
  InitialAlg F
InitialAlgebraTheorem κ {{s}} F coconκF =
  Cocontinuous∧Inflationary→Initial κ F coconκF
  (Iter F κ) (InflIter F κ {{s}})