open import Cubical.Foundations.Prelude

module SignatureAlgebra.Initial.Initiality (ℓi : Level) where

open import Cubical.Foundations.Function
open import Cubical.Foundations.Structure

open import Cubical.Data.Sigma

open import DCPO ℓi

open import SignatureAlgebra.Initial.Base ℓi
open import SignatureAlgebra.Initial.Elimination ℓi
open import SignatureAlgebra.Signature ℓi
open import SignatureAlgebra.SignatureAlgebra ℓi
open import SignatureAlgebra.Monomial ℓi

private
  variable
    ℓa ℓt ℓc ℓmb ℓmc ℓmct ℓe ℓv : Level

module _ {ℓa : Level} {Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv} where
  initiality : (A : SignatureAlgebra Σ ℓa ℓt)
             → isContr (SignatureMorphism (initialSignatureAlgebra Σ) A)
  initiality A = ! , !isUnique
    where
      ! : SignatureMorphism (initialSignatureAlgebra Σ) A
      ! = recMorphism A

      !isUnique : (f : SignatureMorphism (initialSignatureAlgebra Σ) A) → ! ≡ f
      !isUnique f =
        SignatureMorphism≡ (funExt (ind (record { Args })))
        where module Args where
          Y : Initial Σ → Type ℓa
          Y x = function ! x ≡ function f x

          isPropY : (x : Initial Σ) → isProp (Y x)
          isPropY x = sethood (underlyingDCPO A) _ _

          isSupPreservingY : {I : Type ℓi} (α : I → Initial Σ) (δ : isDirected (Leq Σ) α)
                           → ((i : I) → function ! (α i) ≡ function f (α i))
                           → function ! (lub δ) ≡ function f (lub δ)
          isSupPreservingY α δ IH =
            function ! (lub δ)                           ≡⟨ refl ⟩
            ∐ (underlyingDCPO A) {α = rec A ∘ α} δ₁      ≡⟨ ((λ i → ∐ (underlyingDCPO A) {α = p i} (q i))) ⟩
            ∐ (underlyingDCPO A) {α = function f ∘ α} δ₂ ≡⟨ sym (supPreservation (continuousMap f) δ) ⟩
            function f (lub δ) ∎
            where
              p : function ! ∘ α ≡ function f ∘ α
              p = funExt IH

              δ₁ : isDirected (order (underlyingDCPO A)) (rec A ∘ α)
              δ₁ = recImageIsDirected A δ

              δ₂ : isDirected (order (underlyingDCPO A)) (function f ∘ α)
              δ₂ = imageIsDirected (continuousMap f) δ

              q : PathP (λ i → isDirected (order (underlyingDCPO A)) (p i)) δ₁ δ₂
              q = isProp→PathP (λ i → isPropIsDirected (order (underlyingDCPO A)) (p i)) δ₁ δ₂

          isAppPreservingY : (c : constructorNames Σ)
                           → (args : ⟨ ⟦ constructors Σ c ⟧ₘ (initialSignatureDCPO Σ) ⟩)
                           → ⟦ constructors Σ c ⟧ₘᵈᵉᵖ (initialSignatureDCPO Σ) Y args
                           → function ! (app c args) ≡ function f (app c args)
          isAppPreservingY c args IH =
            function ! (app c args)      ≡⟨ refl ⟩
            interpretation A c
              (fmapₘ (constructors Σ c)
                (initialSignatureDCPO Σ)
                (underlyingDCPO A)
                (rec A)
                args)                    ≡⟨ cong (interpretation A c) (fmapₘ≡ (constructors Σ c) (initialSignatureDCPO Σ) (underlyingDCPO A) (rec A) (function f) (funExt (fst IH))) ⟩
            interpretation A c
              (fmapₘ (constructors Σ c)
                (initialSignatureDCPO Σ)
                (underlyingDCPO A)
                (function f)
                args)                    ≡⟨ commutation f c args ⟩
            function f (app c args) ∎