open import Cubical.Foundations.Prelude

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

open import Cubical.Categories.Category
open import Cubical.Categories.Adjoint
open import Cubical.Categories.Functor
open import Cubical.Categories.NaturalTransformation

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

open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Sigma
open import Cubical.Data.Sum as ⊎
open import Cubical.Data.Unit

open import AdjointResults

open import DCPO ℓi
open import DCPO.Category ℓi
open import DCPO.Constructions.BinaryProduct ℓi
open import DCPO.Constructions.Lift ℓi
open import DCPO.Constructions.Product ℓi

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

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

module _ (Σ : Signature ℓc ℓmb ℓmc ℓmct ℓe ℓv) where

  level : Level
  level = initialSignatureAlgebraLevel ℓc ℓmb ℓmc ℓmct ℓe ℓv

  open Functor

  Underlying : Functor (SignatureAlgebraCategory Σ level level) (DCPOCategory level level)
  F-ob Underlying = underlyingDCPO
  F-hom Underlying = continuousMap
  F-id Underlying = refl
  F-seq Underlying f g = refl

  Free₀ : DCPO level level → SignatureAlgebra Σ level level
  Free₀ D = forgetIncl (initialSignatureAlgebra (Σ +ˢⁱᵍ D))

  η : (D : DCPO level level)
    → DCPOMorphism D (Underlying ⟅ Free₀ D ⟆)
  η D = inclContinuousMap (initialSignatureAlgebra (Σ +ˢⁱᵍ D))

  toInclCommutingMorphism : (D : DCPO level level)
                          → (X : SignatureAlgebra Σ level level)
                          → (g : SignatureMorphism (Free₀ D) X)
                          → (f : DCPOMorphism D (underlyingDCPO X))
                          → continuousMap g ∘ᵈᶜᵖᵒ η D ≡ f
                          → SignatureMorphism (initialSignatureAlgebra (Σ +ˢⁱᵍ D)) (addIncl X f)
  toInclCommutingMorphism D X g f p =
    signaturemorphism
      (continuousMap g)
      λ { (inl c) args →
            commutation g c
              (lowerArgs ℓ-zero level level (constructors Σ c)
                (initialSignatureDCPO (Σ +ˢⁱᵍ D)) args)
        ; (inr tt) args →
            sym (funExt⁻ (cong DCPOMorphism.function p) (lower (snd args))) ∙
            cong (function g ∘ interpretation (initialSignatureAlgebra (Σ +ˢⁱᵍ D)) (inr tt))
              (≡-× (isContr→isProp isContrΠ⊥* _ _) refl) }

  private
    universalArrow : (D : DCPO level level) (X : SignatureAlgebra Σ level level)
                  → DCPOMorphism D (underlyingDCPO X)
                  → SignatureMorphism (Free₀ D) X
    universalArrow D X f =
      signaturemorphism
        (recContinuousMap (addIncl X f))
        λ c args →
          recCommutes (addIncl X f) (inl c)
            (liftArgs ℓ-zero level level (constructors Σ c)
              (initialSignatureDCPO (Σ +ˢⁱᵍ D)) args)

    abstract
      universalArrowIsUnique : (D : DCPO level level) (X : SignatureAlgebra Σ level level)
                            → (f : DCPOMorphism D (underlyingDCPO X))
                            → (g : SignatureMorphism (Free₀ D) X)
                            → continuousMap g ∘ᵈᶜᵖᵒ η D ≡ f
                            → universalArrow D X f ≡ g
      universalArrowIsUnique D X f g p =
        SignatureMorphism≡ (cong SignatureMorphism.function q)
        where
          g' : SignatureMorphism (initialSignatureAlgebra (Σ +ˢⁱᵍ D)) (addIncl X f)
          g' = toInclCommutingMorphism D X g f p

          universalArrow' : SignatureMorphism (initialSignatureAlgebra (Σ +ˢⁱᵍ D)) (addIncl X f)
          universalArrow' = toInclCommutingMorphism D X (universalArrow D X f) f (DCPOMorphism≡ refl)

          q : universalArrow' ≡ g'
          q = isContr→isProp (initiality (addIncl X f)) _ _

    adjunctionArgs : MakeLeftAdjoint Underlying
    adjunctionArgs = record
      { L₀ = Free₀
      ; η = η
      ; universal = λ {D} {X} → universalArrow D X
      ; commutes = λ f → DCPOMorphism≡ refl
      ; unique = λ {D} {X} {f} {g} → universalArrowIsUnique D X f g }

  open MakeLeftAdjoint
  open UnitCounit

  Free : Functor (DCPOCategory level level) (SignatureAlgebraCategory Σ level level)
  Free = toFunctor adjunctionArgs

  Free⊣Underlying : Free ⊣ Underlying
  Free⊣Underlying = toAdjoint adjunctionArgs