ImprHIT.SetTruncated.Limits

module ImprHIT.SetTruncated.Limits where

open import Cubical.Categories.Category.Base
open import Cubical.Categories.Constructions.FullSubcategory
open import Cubical.Categories.Functor
open import Cubical.Categories.Instances.FunctorAlgebras
open import Cubical.Categories.Instances.Sets
open import Cubical.Categories.Limits.Limits
open import Cubical.Data.Sigma.Properties
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Prelude hiding (J)

open import ImprHIT.Background.Impredicativity
open import ImprHIT.Background.Weide
open import ImprHIT.SetTruncated.LawfulSetAlgebra

open Algebra
open AlgebraHom
open Category hiding (_∘_)
open Cone
open Functor
open Iso
open LimCone
open PolyTypeConstr
open FinSum

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ
    B : A → Type ℓ
    J : Category ℓ ℓ'
    D : Functor J (SET ℓ-zero)

funToImpr : (∀ x → B x) ≃ Π A B
funToImpr = isoToEquiv $ iso Λ ev Π-η Π-β

isOfHLevelΠimpr : ∀ h → (∀ x → isOfHLevel h (B x)) → isOfHLevel h (Π A B)
isOfHLevelΠimpr h = isOfHLevelRespectEquiv h funToImpr ∘ isOfHLevelΠ h

_* : ∀ {J} → (Functor {ℓ} {ℓ'} J (SET ℓ-zero)) → Type₀
_* {J = J} D = Π (ob J) (fst ∘ F-ob D)

Nat : ∀ D → _* {J = J} D → Type₀
Nat {J = record { ob = J₀ ; Hom[_,_] = J₁[_,_] }} D ϕ =
  Π J₀ λ i → Π J₀ λ j → Π J₁[ i , j ] λ u → F-hom D u (ev ϕ i) ≡ ev ϕ j

natIsProp : (D : Functor J _) → ∀ ϕ → isProp (Nat D ϕ)
natIsProp D ϕ =
  isOfHLevelΠimpr 1 λ _ → isOfHLevelΠimpr 1 λ j → isOfHLevelΠimpr 1 λ _ →
  snd (F-ob D j) _ _

l : (D : Functor J (SET _)) →  Type₀
l D = Σ (D *) (Nat D)

lIsSet : (D : Functor J (SET _)) → isSet (l D)
lIsSet D = isSetΣ (isOfHLevelΠimpr 2 $ snd ∘ F-ob D)
                (isProp→isSet ∘ natIsProp D)

lIsCone : (D : Functor J (SET _)) → Cone D (l D , lIsSet D)
lIsCone _ = cone (λ i x → ev (fst x) i) λ {i j} u → funExt λ (ϕ , ϑ) →
            ev (ev (ev ϑ i) j) u

funExtImpr : {f g : Π A B} → ((x : A) → ev f x ≡ ev g x) → f ≡ g
funExtImpr {f = f} {g = g} h = sym (Π-η f) ∙ cong Λ (funExt h) ∙ Π-η g

lIsTerminal : (D : Functor J (SET _)) → isLimCone D (l D , lIsSet D) (lIsCone D)
lIsTerminal D V M@(cone μ Hμ) =
  (mapToL , mapToLIsConeMorphism) , univConeMorphismIsUnique
  where
  mapToL : fst V → l D
  mapToL v =
    Λ ((_$ v) ∘ μ) ,
    Λ λ i → Λ λ j → Λ λ u →
      F-hom D u (ev (Λ ((_$ v) ∘ μ)) i)
        ≡⟨ refl ⟩
      F-hom D u (μ i v)
        ≡⟨ cong (_$ v) (Hμ u) ⟩
      μ j v
        ≡⟨ refl ⟩
      ev (Λ ((_$ v) ∘ μ)) j ∎
  mapToLIsConeMorphism : isConeMor M (lIsCone D) mapToL
  mapToLIsConeMorphism i = refl
  univConeMorphismIsUnique : (Y : Σ (fst V → l D) (isConeMor M $ lIsCone D)) →
                             (mapToL , mapToLIsConeMorphism) ≡ Y
  univConeMorphismIsUnique (y , k)  = ΣPathPProp
    (λ _ _ _ → isPropΠ (λ i → isSetΠ (λ _ → snd $ F-ob D i) _ _ ) _ _ )
    (funExt λ v → ΣPathPProp
      (natIsProp D) $
      funExtImpr $ funExt⁻ (
        ev (Λ $ (_$ v) ∘ μ) ≡⟨ refl ⟩
        (_$ v) ∘ μ ≡⟨ funExt (λ i → cong (_$ v) $ sym $ k i) ⟩
        ev (fst $ y v) ∎
      )
    ) 

setHasAllLimits : Limits {ℓ} {ℓ'} (SET ℓ-zero)
setHasAllLimits _ D = climCone (l D , lIsSet D) (lIsCone D) (lIsTerminal D)

ForgetLawSetAlg : ∀ S → Functor (LawSetAlg S) (SET ℓ-zero)
ForgetLawSetAlg S = 𝕌 ∘F ι
  where
  𝕌 = ForgetAlgebra (polyFuncOnSet' S)
  ι = FullInclusion (AlgebrasCategory' S) (isLawful S)

lawSetAlgHasAllLimits : ∀ S → Limits {ℓ} {ℓ'} (LawSetAlg S)
lawSetAlgHasAllLimits
  S@((k , H) , n , A , t , r)
  J@(record { ob = J₀ ; Hom[_,_] = J₁[_,_] })
  D using
    D' ← ForgetLawSetAlg S ∘F D |
    V ← (l D' , lIsSet D') |
    M@(cone μ Hμ) ← lIsCone D' |
    γ ← lIsTerminal D' |
    F ← polyFuncOnSet' S
  = climCone (𝕀 , 𝕀IsLawful) 𝕀IsCone 𝕀IsTerminal
  where
  algebraMapCone : ∀ {A} → Cone D' A → Cone D' (F-ob F A)
  algebraMapCone {A} (cone ν Hν) = cone
      (λ i → str (fst $ F-ob D i) ∘ F-hom F (ν i)) λ {i j} u →
      F-hom D' u ∘ str (fst $ F-ob D i) ∘ (F-hom F $ ν i)
        ≡⟨ cong (_∘ F-hom F {A} (ν i)) (strHom $ F-hom D u) ⟩
      str (fst $ F-ob D j) ∘ F-hom F (F-hom D' u) ∘ (F-hom F $ ν i)
        ≡⟨ cong (str (fst $ F-ob D j) ∘_) $ sym $ F-seq F (ν i) (F-hom D' u) ⟩
      str (fst $ F-ob D j) ∘ F-hom F (F-hom D' u ∘ ν i)
        ≡⟨ cong (λ f → str (fst $ F-ob D j) ∘ F-hom F {A} f) (Hν u) ⟩
      str (fst $ F-ob D j) ∘ F-hom F (ν j) ∎
  𝕀 : Algebra F
  𝕀 = algebra V $ fst $ fst $ γ (F-ob F V) $ algebraMapCone M
  α = str 𝕀 
  𝕀IsLawful : isLawful S 𝕀
  𝕀IsLawful j x =
    ΣPathPProp (natIsProp D') $ funExtImpr $ funExt⁻ $ funExt λ i →
    let
      (algebra B β) , HB = F-ob D i
      f = algebraHom _ $ (snd $ fst $ γ (F-ob F V) $ algebraMapCone M) i
    in
    ev (fst $ t j 【 V , α , x 】) i
      ≡⟨ algHom【】 f (t j) ⟩
    t j 【 B , β , (A j [[ (λ q → ev (fst q) i) ]]) x 】
      ≡⟨ HB _ _ ⟩
    r j 【 B , β , (A j [[ (λ q → ev (fst q) i) ]]) x 】
      ≡⟨ sym $ algHom【】 f (r j) ⟩
    ev (fst $ r j 【 V , α , x 】) i ∎
  𝕀IsCone : Cone D (𝕀 , 𝕀IsLawful)
  𝕀IsCone = cone
    (λ j → let (algebra B β) , HB = F-ob D j in
      algebraHom (μ j) ((snd $ fst $ γ (F-ob F V) $ algebraMapCone M) j))
    (AlgebraHom≡ F ∘ Hμ)
  𝕀IsTerminal : isLimCone D (𝕀 , 𝕀IsLawful) 𝕀IsCone
  𝕀IsTerminal 𝔹@(algebra B β , _) Bcone@(cone ν _) using
    Bcone'@(cone ν' _) ← F-cone (ForgetLawSetAlg S) Bcone |
    ((g , Hg) , Kg) ← γ _ Bcone' =
    (algebraHom g (fst $ PathPΣ $ isContr→isProp -- Existence
      (γ (F-ob F B) $ algebraMapCone Bcone')
      (g ∘ β , λ j →
        μ j ∘ g ∘ β
          ≡⟨ cong (_∘ β) (Hg j) ⟩
        ν' j ∘ β
          ≡⟨ strHom (ν j) ⟩
        str (fst $ F-ob D j) ∘ (F-hom F $ ν' j) ∎
      ) $
      α ∘ F-hom F g , λ j →
        μ j ∘ α ∘ F-hom F g
          ≡⟨ cong (_∘ F-hom F {B} g) (strHom $ coneOut 𝕀IsCone j)  ⟩
        str (fst $ F-ob D j) ∘ F-hom F {V} (μ j) ∘ F-hom F g
          ≡⟨ cong (str (fst $ F-ob D j) ∘_) (sym $ F-seq F g $ μ j) ⟩
        str (fst $ F-ob D j) ∘ F-hom F (μ j ∘ g)
          ≡⟨ cong ((str (fst $ F-ob D j) ∘_) ∘ F-hom F) (Hg j) ⟩
        str (fst $ F-ob D j) ∘ (F-hom F $ ν' j) ∎
      ) , AlgebraHom≡ F ∘ Hg) ,
    λ (y , l) → -- Unicity
      ΣPathPProp
        (λ _ → isPropΠ λ j →
          isSetHom (LawSetAlg (_ , n , A , t , r)) {𝔹} {F-ob D j} _ _)
        -- would look nicer is we had F-coneMor in Limits/Limits.agda
        $ AlgebraHom≡ F $ fst $ PathPΣ $ Kg $ carrierHom y , cong carrierHom ∘ l