module InflationaryIteration where

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

----------------------------------------------------------------------
-- Bounded inflationary iteration
----------------------------------------------------------------------

-- The property that a bounded diagram is an inflationary iteration
Inflᵇ :
  {𝓒 : Set₁}
  {{_ : CAT 𝓒}}
  {{_ : Cocomplete 𝓒}}
  (F : 𝓒 → 𝓒)
  {{_ : Functor F}}
  {κ : Set}
  {{_ : Size κ}}
  (i : κ)
  (D : Diagᵇ i 𝓒)
  → ---------------
  Prop₁
Inflᵇ F i D =
  ∀ᵇ j < i , (Vᵇ D j   ≡  colimᵇ j (F ⊙ᵇ (D ⇂ᵇ j)) ∧
  ∀ᵇ k < j , (Eᵇ D j k ≣ colimᵇ⇂ j k (F ⊙ᵇ (D ⇂ᵇ j))))

-- The property of being a bounded inflationary iteration restricts
Inflᵇ⇂ᵇ :
  {𝓒 : Set₁}
  {{_ : CAT 𝓒}}
  {{_ : Cocomplete 𝓒}}
  {F : 𝓒 → 𝓒}
  {{_ : Functor F}}
  {κ : Set}
  {{_ : Size κ}}
  {i j : κ}
  {{_ : j <ᵇ i}}
  (D : Diagᵇ i 𝓒)
  → ------------------------------
  Inflᵇ F i D → Inflᵇ F j (D ⇂ᵇ j)
Inflᵇ⇂ᵇ _ p k = ∧i (∧e₁ (p k)) λ l → ∧e₂ (p k) l

-- Bounded inflationary iterations are unique if they exist
Inflᵇuniq :
  {𝓒 : Set₁}
  {{_ : CAT 𝓒}}
  {{_ : Cocomplete 𝓒}}
  (F : 𝓒 → 𝓒)
  {{_ : Functor F}}
  {κ : Set}
  {{_ : Size κ}}
  (i : κ)
  (D D' : Diagᵇ i 𝓒)
  → ----------------------------------
  Inflᵇ F i D → Inflᵇ F i D' → D ≡ D'
Inflᵇuniq {𝓒} F {κ} = <ind P p
  where
  P : κ → Prop₁
  P i =
    (D D' : Diagᵇ i 𝓒)
    → ----------------------------------
    Inflᵇ F i D → Inflᵇ F i D' → D ≡ D'

  p : ∀ i → (∀ᵇ j < i , P j) → P i
  p i h D D' q q' = Diagᵇext v e
    where
    v : ∀ᵇ j < i , (Vᵇ D j ≡ Vᵇ D' j)
    v j =
      proof
        Vᵇ D j
      =[ ∧e₁ (q j) ]
        colimᵇ j (F ⊙ᵇ (D ⇂ᵇ j))
      =[ ap
         (λ X → colimᵇ j (F ⊙ᵇ X))
         (h j (D ⇂ᵇ j) (D' ⇂ᵇ j) (Inflᵇ⇂ᵇ D q) (Inflᵇ⇂ᵇ D' q')) ]
        colimᵇ j (F ⊙ᵇ (D' ⇂ᵇ j))
      =[ symm (∧e₁ (q' j)) ]
        Vᵇ D' j
      qed

    e : ∀ᵇ j < i , ∀ᵇ k < j , (Eᵇ D j k ≣ Eᵇ D' j k)
    e j k =
      proof
        Eᵇ D j k
      =[ ∧e₂ (q j) k ]
        colimᵇ⇂ j k (F ⊙ᵇ (D ⇂ᵇ j))
      =[ ap
         (λ X → colimᵇ⇂ j k (F ⊙ᵇ X))
         (h j (D ⇂ᵇ j) (D' ⇂ᵇ j) (Inflᵇ⇂ᵇ D q) (Inflᵇ⇂ᵇ D' q')) ]
        colimᵇ⇂ j k (F ⊙ᵇ (D' ⇂ᵇ j))
      =[ symm (∧e₂ (q' j) k) ]
        Eᵇ D' j k
      qed

-- There is a bounded inflationary iteration
module _
  {𝓒 : Set₁}
  {{_ : CAT 𝓒}}
  {{_ : Cocomplete 𝓒}}
  (F : 𝓒 → 𝓒)
  {{_ : Functor F}}
  {κ : Set}
  {{_ : Size κ}}
  where
  private
    A : κ → Set₁
    A i = set D ∶ Diagᵇ i 𝓒 , Inflᵇ F i D

    α : ∀ i → (∏ᵇ j < i , A j) → A i
    α i h = D ∣ δ
      where
      h⇂ᵇ :
        (j k : κ)
        {{_ : j <ᵇ i}}
        {{_ : k <ᵇ j}}
        → -----------------------
        el (h j) ⇂ᵇ k ≡ el (h k)
      h⇂ᵇ j k =
        Inflᵇuniq F k (el (h j) ⇂ᵇ k) (el (h k))
        (Inflᵇ⇂ᵇ (el (h j)) (pf (h j))) (pf (h k))

      VᵇD : ∏ᵇ j < i , 𝓒
      VᵇD j = colimᵇ j (F ⊙ᵇ (el (h j)))

      EᵇD : ∏ᵇ j < i , ∏ᵇ k < j , (VᵇD k ⟶ VᵇD j)
      EᵇD j k =
        subst (λ X → colimᵇ k (F ⊙ᵇ X) ⟶ colimᵇ j (F ⊙ᵇ el (h j)))
        (h⇂ᵇ j k) (colimᵇ⇂ j k (F ⊙ᵇ (el (h j))))

      EᵇD∙incᵇ : ∀ᵇ j < i , ∀ᵇ k < j , ∀ᵇ l < k ,
        (incᵇ (F ⊙ᵇ (el (h j))) l ≣ EᵇD j k ∙ incᵇ (F ⊙ᵇ (el (h k))) l)
      EᵇD∙incᵇ j k l =
        proof
          incᵇ (F ⊙ᵇ el (h j)) l
        =[ colimᵇ⇂incᵇ j k l (F ⊙ᵇ el (h j)) ]
          colimᵇ⇂ j k (F ⊙ᵇ el (h j)) ∙ incᵇ ((F ⊙ᵇ el (h j)) ⇂ᵇ k) l
        =[ ∙cong _ _ _ _
               (ap (λ D' → F (Vᵇ D' l)) (h⇂ᵇ j k))
               (ap (λ D' → colimᵇ k (F ⊙ᵇ D')) (h⇂ᵇ j k))
               refl
               (ap (λ D' → incᵇ (F ⊙ᵇ D') l) (h⇂ᵇ j k))
               (symm (subst≣
               (λ X → colimᵇ k (F ⊙ᵇ X) ⟶ colimᵇ j (F ⊙ᵇ el (h j)))
               (h⇂ᵇ j k) _)) ]
          EᵇD j k ∙ incᵇ (F ⊙ᵇ el (h k)) l
        qed

      Eᵇ∙EᵇD : ∀ᵇ j < i , ∀ᵇ k < j , ∀ᵇ l < k ,
        (EᵇD j k ∙ EᵇD k l ≡ EᵇD j l)
      Eᵇ∙EᵇD j k l = colimextᵇ (F ⊙ᵇ (el (h l))) λ m →
        (proof
           (EᵇD j k ∙ EᵇD k l) ∙ incᵇ (F ⊙ᵇ el (h l)) m
         =[ ∙assoc ]
           EᵇD j k ∙ (EᵇD k l ∙ incᵇ (F ⊙ᵇ el (h l)) m)
         =[ ∙cong _ _ _ _
             (proof
                F (Vᵇ (el (h l)) m)
              =[ ap (λ D' → F (Vᵇ D' m)) (symm (h⇂ᵇ j l)) ]
                F (Vᵇ (el (h j)) m)
              =[ ap (λ D' → F (Vᵇ D' m)) (h⇂ᵇ j k) ]
                F (Vᵇ (el (h k)) m)
              qed)
              refl
              refl
              (symm (EᵇD∙incᵇ k l m))
              refl ]
           EᵇD j k ∙ incᵇ (F ⊙ᵇ (el (h k))) m
         =[ symm (EᵇD∙incᵇ j k m) ]
           incᵇ (F ⊙ᵇ (el (h j))) m
         =[ EᵇD∙incᵇ j l m ]
           EᵇD j l ∙ incᵇ (F ⊙ᵇ el (h l)) m
         qed)

      D : Diagᵇ i 𝓒
      D = record { Vᵇ = VᵇD ; Eᵇ = EᵇD ; Eᵇ∙Eᵇ = Eᵇ∙EᵇD  }

      D⇂ᵇ : ∀ᵇ j < i , (el (h j) ≡ D ⇂ᵇ j)
      D⇂ᵇ j = Diagᵇext
        (λ k →
          (proof
             Vᵇ (el (h j)) k
           =[ ∧e₁ (pf (h j) k) ]
             colimᵇ k (F ⊙ᵇ (el (h j) ⇂ᵇ k))
           =[ ap
              (λ X → colimᵇ k (F ⊙ᵇ X)) (h⇂ᵇ j k) ]
             colimᵇ k (F ⊙ᵇ el (h k))
           qed))
        (λ k l →
          (proof
             Eᵇ (el (h j)) k l
           =[ ∧e₂ (pf (h j) k) l ]
             colimᵇ⇂ k l (F ⊙ᵇ (el (h j) ⇂ᵇ k))
           =[ ap (λ X → colimᵇ⇂ k l (F ⊙ᵇ X)) (h⇂ᵇ j k) ]
             colimᵇ⇂ k l (F ⊙ᵇ el (h k))
           =[ symm (subst≣
              (λ X → colimᵇ l (F ⊙ᵇ X) ⟶ colimᵇ k (F ⊙ᵇ el (h k)))
              (h⇂ᵇ k l) _) ]
             Eᵇ D k l
           qed))

      δ : Inflᵇ F i D
      δ j =
        ∧i (ap (λ X → colimᵇ j (F ⊙ᵇ X)) (D⇂ᵇ j))
        (λ k →
          (proof
             Eᵇ D j k
           =[ subst≣
                (λ X → colimᵇ k (F ⊙ᵇ X) ⟶ colimᵇ j (F ⊙ᵇ el (h j)))
                (h⇂ᵇ j k) _ ]
             colimᵇ⇂ j k (F ⊙ᵇ (el (h j)))
           =[ ap (λ X → colimᵇ⇂ j k (F ⊙ᵇ X)) (D⇂ᵇ j) ]
             colimᵇ⇂ j k (F ⊙ᵇ (D ⇂ᵇ j))
           qed))


  Iterᵇ : (i : κ) → Diagᵇ i 𝓒
  Iterᵇ i = el (<rec A α i)

  InflᵇIterᵇ : ∀ i → Inflᵇ F i (Iterᵇ i)
  InflᵇIterᵇ i = pf (<rec A α i)

  Iterᵇ⇂ : ∀ i → ∀ᵇ j < i , ((Iterᵇ i) ⇂ᵇ j ≡ Iterᵇ j)
  Iterᵇ⇂ i j =
    Inflᵇuniq F j ((Iterᵇ i) ⇂ᵇ j) (Iterᵇ j)
    (Inflᵇ⇂ᵇ (Iterᵇ i) (InflᵇIterᵇ i)) (InflᵇIterᵇ j)

----------------------------------------------------------------------
-- Inflationary iteration
----------------------------------------------------------------------
-- The property that a diagram is an inflationary iteration
Infl :
  {𝓒 : Set₁}
  {{_ : CAT 𝓒}}
  {{_ : Cocomplete 𝓒}}
  (F : 𝓒 → 𝓒)
  {{_ : Functor F}}
  (κ : Set)
  {{_ : Size κ}}
  → ------------------
  Diag κ 𝓒 → Prop₁
Infl F κ D =
  ∀ i → V D i ≡  colimᵇ i (F ⊙ᵇ (D ⇂ i))
  ∧
  ∀ᵇ j < i , (E D i j ≣ colimᵇ⇂ i j (F ⊙ᵇ (D ⇂ i)))

-- Lemma 3.6 : There is an inflationary iteration
module _
  {𝓒 : Set₁}
  {{_ : CAT 𝓒}}
  {{_ : Cocomplete 𝓒}}
  (F : 𝓒 → 𝓒)
  {{_ : Functor F}}
  (κ : Set)
  {{_ : Size κ}}
  where
  private
    VIter : κ → 𝓒
    VIter i = colimᵇ i (F ⊙ᵇ (Iterᵇ F i))

    VIter⇂ : ∀ i → ∀ᵇ j < i ,
      (colimᵇ j ((F ⊙ᵇ Iterᵇ F i) ⇂ᵇ j) ≡ VIter j)
    VIter⇂ i j = ap (λ X → colimᵇ j (F ⊙ᵇ X)) (Iterᵇ⇂ F i j)

    EIter : ∀ i → ∏ᵇ j < i , (VIter j ⟶ VIter i)
    EIter i j =
      subst (_⟶ VIter i) (VIter⇂ i j) (colimᵇ⇂ i j (F ⊙ᵇ Iterᵇ F i))

    abstract
      EIter∙incᵇ : ∀ i → ∀ᵇ j < i , ∀ᵇ k < j ,
        (incᵇ (F ⊙ᵇ Iterᵇ F i) k ≣ EIter i j ∙ incᵇ (F ⊙ᵇ Iterᵇ F j) k)
      EIter∙incᵇ i j k =
        proof
          incᵇ (F ⊙ᵇ (Iterᵇ F i)) k
        =[ colimᵇ⇂incᵇ i j k (F ⊙ᵇ Iterᵇ F i) ]
          colimᵇ⇂ i j (F ⊙ᵇ Iterᵇ F i) ∙  incᵇ ((F ⊙ᵇ Iterᵇ F i) ⇂ᵇ j) k
        =[ ∙cong _ _ _ _
             (ap (λ D' → F (Vᵇ D' k)) (Iterᵇ⇂ F i j))
             (ap (λ D' → colimᵇ j (F ⊙ᵇ D')) (Iterᵇ⇂ F i j))
             refl
             (ap (λ D' → incᵇ (F ⊙ᵇ D') k) (Iterᵇ⇂ F i j))
             (symm (subst≣ (_⟶ VIter i)
               (ap (λ D' → colimᵇ j (F ⊙ᵇ D')) (Iterᵇ⇂ F i j)) _)) ]
           EIter i j ∙ incᵇ (F ⊙ᵇ (Iterᵇ F j)) k
        qed

      E∙EIter : ∀ i → ∀ᵇ j < i , ∀ᵇ k < j ,
        (EIter i j ∙ EIter j k ≡ EIter i k)
      E∙EIter i j k = colimextᵇ (F ⊙ᵇ (Iterᵇ F k)) λ l →
        (∙assoc ；
         (∙cong _ _ _ _
            (ap (λ D' → F (Vᵇ D' l)) (symm (Iterᵇ⇂ F j k)))
            refl
            refl
            (symm (EIter∙incᵇ j k l))
            refl)；
         symm (EIter∙incᵇ i j l)；
         EIter∙incᵇ i k l )
        -- proof
        --   (EIter i j ∙ EIter j k) ∙ incᵇ (F ⊙ᵇ Iterᵇ F k) l
        -- =[ ∙assoc ]
        --   EIter i j ∙ (EIter j k ∙ incᵇ (F ⊙ᵇ Iterᵇ F k) l)
        -- =[ ∙cong _ _ _ _
        --     (ap (λ D' → F (Vᵇ D' l)) (symm (Iterᵇ⇂ F j k)))
        --     refl
        --     refl
        --     (symm (EIter∙incᵇ j k l))
        --     refl ]
        --   EIter i j ∙ incᵇ (F ⊙ᵇ Iterᵇ F j) l
        -- =[ symm (EIter∙incᵇ i j l) ]
        --   incᵇ (F ⊙ᵇ Iterᵇ F i) l
        -- =[ EIter∙incᵇ i k l ]
        --   EIter i k ∙ incᵇ (F ⊙ᵇ Iterᵇ F k) l
        -- qed

  Iter : Diag κ 𝓒
  Iter = record { V = VIter ; E = EIter ; E∙E = E∙EIter }

  abstract
    Iter⇂ : ∀ i → Iterᵇ F i ≡ Iter ⇂ i
    Iter⇂ i = Diagᵇext
      (λ j → ∧e₁ (InflᵇIterᵇ F i j) ； VIter⇂ i j)
        -- proof
        --   Vᵇ (Iterᵇ F i) j
        -- =[ ∧e₁ (InflᵇIterᵇ F i j) ]
        --   colimᵇ j ((F ⊙ᵇ Iterᵇ F i) ⇂ᵇ j)
        -- =[ VIter⇂ i j ]
        --   colimᵇ j (F ⊙ᵇ Iterᵇ F j)
        -- qed
      (λ j k →
        ∧e₂ (InflᵇIterᵇ F i j) k ；
        ap (λ X → colimᵇ⇂ j k (F ⊙ᵇ X)) (Iterᵇ⇂ F i j) ；
        symm (subst≣ (_⟶ VIter j) (VIter⇂ j k) _))
        -- proof
        --   Eᵇ (Iterᵇ F i) j k
        -- =[  ∧e₂ (InflᵇIterᵇ F i j) k ]
        --   colimᵇ⇂ j k (F ⊙ᵇ (Iterᵇ F i ⇂ᵇ j))
        -- =[ ap (λ X → colimᵇ⇂ j k (F ⊙ᵇ X)) (Iterᵇ⇂ F i j) ]
        --   colimᵇ⇂ j k (F ⊙ᵇ Iterᵇ F j)
        -- =[ symm (subst≣ (_⟶ VIter j) (VIter⇂ j k) _) ]
        --   EIter j k
        -- qed

    InflIter : Infl F κ Iter
    InflIter i =
      ∧i (ap (λ X → colimᵇ i (F ⊙ᵇ X)) (Iter⇂ i))
        (λ j →
          subst≣ (λ X → X ⟶ VIter i) (VIter⇂ i j) _ ；
          ap (λ X → colimᵇ⇂ i j (F ⊙ᵇ X)) (Iter⇂ i))
        -- proof
        --   E Iter i j
        -- =[ subst≣ (λ X → X ⟶ VIter i) (VIter⇂ i j) _ ]
        --   colimᵇ⇂ i j (F ⊙ᵇ Iterᵇ F i)
        -- =[ ap (λ X → colimᵇ⇂ i j (F ⊙ᵇ X)) (Iter⇂ i) ]
        --   colimᵇ⇂ i j (F ⊙ᵇ (Iter ⇂ i))
        -- qed