module ImprHIT.SetTruncated.Initial where

open import Cubical.Categories.Category.Base
open import Cubical.Categories.Functor
open import Cubical.Categories.Instances.FunctorAlgebras
open import Cubical.Categories.Limits.Initial
open import Cubical.Categories.Limits.Limits
open import Cubical.Data.Sigma.Properties
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Prelude

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

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

private
  variable
    ℓ ℓ' : Level

isInitial→isLimIdCone : ∀ (C : Category ℓ ℓ') I ->
                       isInitial C I → Σ (Cone 𝟙⟨ C ⟩ I) (isLimCone 𝟙⟨ C ⟩ I)
isInitial→isLimIdCone C I h =
  let p = fst ∘ h
      γ = cone p (λ {v = X} _ → isContr→isProp (h X) _ _)
  in γ , -- cone
     λ J (cone q Hq) → -- second cone
       uniqueExists (q I) (Hq ∘ p)
       (isPropIsConeMor (cone q Hq) γ)
       λ y Hy →
         q I
           ≡⟨ sym (Hy I) ⟩
         y ⋆⟨ C ⟩ p I
           ≡⟨ cong (seq' C y) $
              initialEndoIsId C (I , h) (p I) ⟩
         y ⋆⟨ C ⟩ id C
           ≡⟨ ⋆IdR C y ⟩
         y ∎

isLimIdCone→isInitial : ∀ (C : Category ℓ ℓ') X ->
                       Σ (Cone 𝟙⟨ C ⟩ X) (isLimCone 𝟙⟨ C ⟩ X) -> isInitial C X
isLimIdCone→isInitial C I (cone p Hp , H) X = p X , λ y →
  p X
    ≡⟨ sym (Hp y) ⟩
  p I ⋆⟨ C ⟩ y
    ≡⟨ cong (λ x → x ⋆⟨ C ⟩ y) pIIsIdentity ⟩
  id C ⋆⟨ C ⟩ y
    ≡⟨ ⋆IdL C y ⟩ y ∎
  where -- There's only one endomorphism on the terminal cone, so p I ≡ id C
  pIConeEndomorphism = p I , Hp ∘ p
  idCConeEndomorphism = id C , isConeMorId {D = 𝟙⟨ C ⟩} (cone p Hp)
  pIIsIdentity : p I ≡ id C
  pIIsIdentity = fst $ PathPΣ $ (isContr→isProp $ H I $ cone p Hp)
                 pIConeEndomorphism idCConeEndomorphism

InitialLawSetAlg : ∀ S → Initial (LawSetAlg S)
InitialLawSetAlg S using
  F ← polyFuncOnSet' S |
  climCone I γ Hγ ← lawSetAlgHasAllLimits S (LawSetAlg S) (𝟙⟨ LawSetAlg S ⟩)
  = I , isLimIdCone→isInitial (LawSetAlg S) I (γ , Hγ)

InitialLawSetAlgebraCarrier : Sig  → hSet ℓ-zero
InitialLawSetAlgebraCarrier = carrier ∘ fst ∘ fst ∘ InitialLawSetAlg