open import Cubical.Foundations.Prelude

module SignatureAlgebra.Examples.CoalescedSum (ℓi : Level) where

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.Unit

open import Cubical.HITs.PropositionalTruncation as ∥₁

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

open import SignatureAlgebra.Initial ℓi as InitialΣAlg
open import SignatureAlgebra.Monomial ℓi
open import SignatureAlgebra.Signature ℓi
open import SignatureAlgebra.SignatureAlgebra ℓi

open import SignatureAlgebra.Examples.PointedDCPO ℓi

private
  variable
    ℓd ℓt ℓe ℓt' ℓx ℓt'' ℓf : Level

module _ (D : PointedDCPO ℓd ℓt) (E : PointedDCPO ℓe ℓt') where
  data ConstructorName : Type where
    inlᶜ : ConstructorName
    inrᶜ : ConstructorName

  inlₘ : Monomial ℓ-zero (ℓ-max ℓd ℓe) (ℓ-max ℓt ℓt')
  inlₘ = constantₘ (liftDCPO ℓe ℓt' (D ⁻))

  inrₘ : Monomial ℓ-zero (ℓ-max ℓd ℓe) (ℓ-max ℓt ℓt')
  inrₘ = constantₘ (liftDCPO ℓd ℓt (E ⁻))

  coalescedSumPreΣ : PreSignature ℓ-zero ℓ-zero (ℓ-max ℓd ℓe) (ℓ-max ℓt ℓt')
  coalescedSumPreΣ =
    presignature ConstructorName
      λ { inlᶜ → inlₘ
        ; inrᶜ → inrₘ }

  data InequalityName : Type where
    inl⊥⊑inr⊥ : InequalityName
    inr⊥⊑inl⊥ : InequalityName

  inlₜ : {V : Type} → ⟨ D ⟩ → Term coalescedSumPreΣ V
  inlₜ d = constr inlᶜ ⊥.rec (lift d)

  inrₜ : {V : Type} → ⟨ E ⟩ → Term coalescedSumPreΣ V
  inrₜ e = constr inrᶜ ⊥.rec (lift e)

  coalescedSumΣ : Signature ℓ-zero ℓ-zero (ℓ-max ℓd ℓe) (ℓ-max ℓt ℓt') ℓ-zero ℓ-zero
  coalescedSumΣ =
      signature coalescedSumPreΣ InequalityName
        λ { inl⊥⊑inr⊥ →
              inequality ⊥
                (inlₜ (least D))
                (inrₜ (least E))
          ; inr⊥⊑inl⊥ →
              inequality ⊥
                (inrₜ (least E))
                (inlₜ (least D)) }

  CoalescedSumAlgebra : (ℓ ℓ' : Level) → Type (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) (ℓ-suc ℓ)) (ℓ-suc ℓ')) (ℓ-max ℓd ℓe)) (ℓ-max ℓt ℓt'))
  CoalescedSumAlgebra = SignatureAlgebra coalescedSumΣ

  coalescedsumalgebra : (X : DCPO ℓx ℓt'')
                      → (inl : ⟨ D ⟩ → ⟨ X ⟩)
                      → (inr : ⟨ E ⟩ → ⟨ X ⟩)
                      → isContinuous (D ⁻) X inl
                      → isContinuous (E ⁻) X inr
                      → inl (least D) ≡ inr (least E)
                      → CoalescedSumAlgebra ℓx ℓt''
  coalescedsumalgebra X inl inr inlCont inrCont p =
    signaturealgebra
      (presignaturealgebra X
        (λ { inlᶜ → inl ∘ lower ∘ snd
           ; inrᶜ → inr ∘ lower ∘ snd })
        (λ { inlᶜ →
              isContinuous-∘ (⟦ inlₘ ⟧ₘ X) (D ⁻) X inl (lower ∘ snd) inlCont
                (isContinuous-∘ (⟦ inlₘ ⟧ₘ X) (liftDCPO ℓe ℓt' (D ⁻)) (D ⁻)
                  lower snd
                  (lowerIsContinuous _ _ (D ⁻))
                  (sndIsContinuous (Πᵈᶜᵖᵒ ⊥ (λ _ → X)) (liftDCPO _ _ (D ⁻))))
           ; inrᶜ →
              isContinuous-∘ (⟦ inrₘ ⟧ₘ X) (E ⁻) X inr (lower ∘ snd) inrCont
                (isContinuous-∘ (⟦ inrₘ ⟧ₘ X) (liftDCPO ℓd ℓt (E ⁻)) (E ⁻)
                  lower snd
                  (lowerIsContinuous _ _ (E ⁻))
                  (sndIsContinuous (Πᵈᶜᵖᵒ ⊥ (λ _ → X)) (liftDCPO _ _ (E ⁻)))) }))
      λ { inl⊥⊑inr⊥ ρ → ≡→⊑ X p
        ; inr⊥⊑inl⊥ ρ → ≡→⊑ X (sym p) }

  ⟦inlₜ⟧-≡ : {V : Type} (X : CoalescedSumAlgebra ℓx ℓt'') {ρ : V → ⟨ X ⟩} {d : ⟨ D ⟩}
           → ⟦ inlₜ d ⟧ₜ (underlyingDCPO X) (interpretation X) ρ
           ≡ interpretation X inlᶜ (⊥.rec , lift d)
  ⟦inlₜ⟧-≡ X = cong (interpretation X inlᶜ) (≡-× (isContr→isProp isContr⊥→A _ _) refl)

  ⟦inrₜ⟧-≡ : {V : Type} (X : CoalescedSumAlgebra ℓx ℓt'') {ρ : V → ⟨ X ⟩} {e : ⟨ E ⟩}
           → ⟦ inrₜ e ⟧ₜ (underlyingDCPO X) (interpretation X) ρ
           ≡ interpretation X inrᶜ (⊥.rec , lift e)
  ⟦inrₜ⟧-≡ X = cong (interpretation X inrᶜ) (≡-× (isContr→isProp isContr⊥→A _ _) refl)

  initialCoalescedSumAlgebra : CoalescedSumAlgebra (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) ℓd) ℓt) ℓe) ℓt') (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) ℓd) ℓt) ℓe) ℓt')
  initialCoalescedSumAlgebra = initialSignatureAlgebra coalescedSumΣ

  _+ₛ_ : PointedDCPO (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) ℓd) ℓt) ℓe) ℓt') (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) ℓd) ℓt) ℓe) ℓt')
  _+ₛ_ =
    pointeddcpo (initialSignatureDCPO coalescedSumΣ)
      (app inlᶜ (⊥.rec , lift (least D)))
      (InitialΣAlg.ind (record { Args }))
    where module Args where
      Y : Initial coalescedSumΣ → Type (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) ℓd) ℓt) ℓe) ℓt')
      Y x = app inlᶜ (⊥.rec , lift (least D)) ⊑[ coalescedSumΣ ] x

      isPropY : (x : Initial coalescedSumΣ) → isProp (Y x)
      isPropY x = isPropLeq (app inlᶜ (⊥.rec , lift (least D))) x

      isSupPreservingY : {I : Type ℓi} (α : I → Initial coalescedSumΣ)
                       → (δ : isDirected (Leq coalescedSumΣ) α)
                       → ((i : I) → Y (α i))
                       → Y (lub δ)
      isSupPreservingY α δ IH =
        ∥₁.rec (isPropY _)
          (λ i → leqTrans _ (α i) _ (IH i) (lubIsUpperbound δ i))
          (inhabitedIfDirected (Leq coalescedSumΣ) δ)

      isAppPreservingY : (c  : ConstructorName)
                       → (args : ⟨ ⟦ constructors coalescedSumΣ c ⟧ₘ (initialSignatureDCPO coalescedSumΣ) ⟩)
                       → ⟦ constructors coalescedSumΣ c ⟧ₘᵈᵉᵖ (initialSignatureDCPO coalescedSumΣ) Y args
                       → Y (app c args)
      isAppPreservingY inlᶜ args IH =
        isContinuous→isMonotone
          (⟦ constructors coalescedSumΣ inlᶜ ⟧ₘ (initialSignatureDCPO coalescedSumΣ))
          (initialSignatureDCPO coalescedSumΣ)
          (app inlᶜ) (appIsContinuous inlᶜ)
          (≡→⊑ (Πᵈᶜᵖᵒ ⊥ (λ _ → initialSignatureDCPO coalescedSumΣ)) (isContr→isProp isContr⊥→A _ _) ,
           lift (leastIsLeast D _))
      isAppPreservingY inrᶜ args IH = leqTrans _ _ _ ⦅1⦆ ⦅2⦆
        where
          ⦅1⦆ : app inlᶜ (⊥.rec , lift (least D))
               ⊑[ coalescedSumΣ ]
               app inrᶜ (⊥.rec , lift (least E))
          ⦅1⦆ = subst2 (Leq coalescedSumΣ)
                (⟦inlₜ⟧-≡ (initialSignatureAlgebra coalescedSumΣ))
                (⟦inrₜ⟧-≡ (initialSignatureAlgebra coalescedSumΣ))
                (inequality inl⊥⊑inr⊥ ⊥.rec)

          ⦅2⦆ : app inrᶜ (⊥.rec , lift (least E)) ⊑[ coalescedSumΣ ] app inrᶜ args
          ⦅2⦆ = isContinuous→isMonotone
                (⟦ constructors coalescedSumΣ inrᶜ ⟧ₘ (initialSignatureDCPO coalescedSumΣ))
                (initialSignatureDCPO coalescedSumΣ)
                (app inrᶜ) (appIsContinuous inrᶜ)
                (≡→⊑ (Πᵈᶜᵖᵒ ⊥ (λ _ → initialSignatureDCPO coalescedSumΣ)) (isContr→isProp isContr⊥→A _ _) ,
                lift (leastIsLeast E _))

module _ {D : PointedDCPO ℓd ℓt} {E : PointedDCPO ℓe ℓt'} (X : CoalescedSumAlgebra D E ℓx ℓt'') where
  inl : ⟨ D ⟩ → ⟨ X ⟩
  inl = interpretation X inlᶜ ∘ pairing (const ⊥.rec) lift

  inr : ⟨ E ⟩ → ⟨ X ⟩
  inr = interpretation X inrᶜ ∘ pairing (const ⊥.rec) lift

  inlIsContinuous : isContinuous (D ⁻) (underlyingDCPO X) inl
  inlIsContinuous =
    isContinuous-∘ (D ⁻) (⟦ inlₘ D E ⟧ₘ (underlyingDCPO X)) (underlyingDCPO X)
      (interpretation X inlᶜ) (pairing (const ⊥.rec) lift)
      (interpretationIsContinuous X inlᶜ)
      (pairingIsContinuous (D ⁻) (Πᵈᶜᵖᵒ ⊥ (λ _ → underlyingDCPO X)) (liftDCPO ℓe ℓt' (D ⁻))
        (const ⊥.rec) lift
        (constIsContinuous (D ⁻) (Πᵈᶜᵖᵒ ⊥ (λ _ → underlyingDCPO X)))
        (liftIsContinuous _ _ (D ⁻)))

  inrIsContinuous : isContinuous (E ⁻) (underlyingDCPO X) inr
  inrIsContinuous =
    isContinuous-∘ (E ⁻) (⟦ inrₘ D E ⟧ₘ (underlyingDCPO X)) (underlyingDCPO X)
      (interpretation X inrᶜ) (pairing (const ⊥.rec) lift)
      (interpretationIsContinuous X inrᶜ)
      (pairingIsContinuous (E ⁻) (Πᵈᶜᵖᵒ ⊥ (λ _ → underlyingDCPO X)) (liftDCPO ℓd ℓt (E ⁻))
        (const ⊥.rec) lift
        (constIsContinuous (E ⁻) (Πᵈᶜᵖᵒ ⊥ (λ _ → underlyingDCPO X)))
        (liftIsContinuous _ _ (E ⁻)))

module _ {D : PointedDCPO ℓd ℓt} {E : PointedDCPO ℓe ℓt'} {F : PointedDCPO ℓf ℓt''}
         (f : StrictMorphism D F) (g : StrictMorphism E F) where

  FasCoalescedSumAlgebra : CoalescedSumAlgebra D E ℓf ℓt''
  FasCoalescedSumAlgebra =
    coalescedsumalgebra D E (F ⁻) (function f) (function g)
      (continuity (continuousMap f)) (continuity (continuousMap g))
      (strictMorphismIsStrict f ∙ sym (strictMorphismIsStrict g))

  copairing : StrictMorphism (D +ₛ E) F
  copairing =
    strictmorphism (InitialΣAlg.rec FasCoalescedSumAlgebra)
      (InitialΣAlg.recIsContinuous FasCoalescedSumAlgebra)
      (strictMorphismIsStrict f)

  copairingCommutes : (function copairing ∘ inl (initialCoalescedSumAlgebra D E) ≡ function f)
                    × (function copairing ∘ inr (initialCoalescedSumAlgebra D E) ≡ function g)
  copairingCommutes = refl , refl

  copairingIsUnique : (h : StrictMorphism (D +ₛ E) F)
                    → function h ∘ inl (initialCoalescedSumAlgebra D E) ≡ function f
                    → function h ∘ inr (initialCoalescedSumAlgebra D E) ≡ function g
                    → copairing ≡ h
  copairingIsUnique h p q = SignatureMorphism≡ (funExt (ind (record { Args })))
    where module Args where
      Y : Initial (coalescedSumΣ D E) → Type ℓf
      Y x = function copairing x ≡ function h x

      isPropY : (x : Initial (coalescedSumΣ D E)) → isProp (Y x)
      isPropY x = sethood (underlyingDCPO F) _ _

      isSupPreservingY : {I : Type ℓi} (α : I → Initial (coalescedSumΣ D E))
                       → (δ : isDirected (Leq (coalescedSumΣ D E)) α)
                       → ((i : I) → Y (α i))
                       → Y (lub δ)
      isSupPreservingY α δ IH =
        function copairing (lub δ) ≡⟨ refl ⟩
        ∐ (F ⁻) δ₁ ≡⟨ congP (λ i → ∐ (F ⁻)) r ⟩
        ∐ (F ⁻) δ₂ ≡⟨ sym (supPreservation (continuousMap h) δ) ⟩
        function h (lub δ) ∎
        where
          δ₁ : isDirected (order (F ⁻)) (function copairing ∘ α)
          δ₁ = recImageIsDirected FasCoalescedSumAlgebra δ

          δ₂ : isDirected (order (F ⁻)) (function h ∘ α)
          δ₂ = imageIsDirected (continuousMap h) δ

          r : PathP (λ i → isDirected (order (F ⁻)) (funExt IH i)) δ₁ δ₂
          r = isProp→PathP
                (λ i → isPropIsDirected (order (F ⁻)) (funExt IH i))
                δ₁ δ₂

      isAppPreservingY : (c : ConstructorName D E)
                       → (args : ⟨ ⟦ constructors (coalescedSumΣ D E) c ⟧ₘ (initialSignatureDCPO (coalescedSumΣ D E)) ⟩)
                       → ⟦ constructors (coalescedSumΣ D E) c ⟧ₘᵈᵉᵖ (initialSignatureDCPO (coalescedSumΣ D E)) Y args
                       → Y (app c args)
      isAppPreservingY inlᶜ args IH =
        function copairing (app inlᶜ args)       ≡⟨ refl ⟩
        function f (lower (snd args))            ≡⟨ sym (funExt⁻ p (lower (snd args))) ⟩
        function h (app inlᶜ (⊥.rec , snd args)) ≡⟨ cong (function h ∘ app inlᶜ) (≡-× (isContr→isProp isContr⊥→A _ _) refl) ⟩
        function h (app inlᶜ args) ∎
      isAppPreservingY inrᶜ args IH =
        function copairing (app inrᶜ args)       ≡⟨ refl ⟩
        function g (lower (snd args))            ≡⟨ sym (funExt⁻ q (lower (snd args))) ⟩
        function h (app inrᶜ (⊥.rec , snd args)) ≡⟨ cong (function h ∘ app inrᶜ) (≡-× (isContr→isProp isContr⊥→A _ _) refl) ⟩
        function h (app inrᶜ args) ∎