module ImprHIT.SetTruncated.LawfulSetAlgebra 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.Data.FinData.Base
open import Cubical.Data.Sigma.Properties
open import Cubical.Data.Sum.Base
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Prelude hiding (J)
open import Cubical.Functions.Embedding

open import ImprHIT.Background.Impredicativity
open import ImprHIT.Background.Weide

open Functor
open FinSum

private
  data ℕ/3ℕ : Type₀ where
    𝟘 : ℕ/3ℕ
    𝕊 : ℕ/3ℕ → ℕ/3ℕ
    mod : 𝟘 ≡ 𝕊 (𝕊 (𝕊 𝟘))

algHom【】 : ∀ {k} {H : Fin k → PolyTypeConstr ℓ-zero 0} {G P}
          {𝔸@(algebra A α) 𝔹@(algebra B β) : Algebra (⨁ H)}
          {x} ((algebraHom f h) : AlgebraHom _ 𝔸 𝔹)
          (r : PathConstructorTerm H G P) →
          (P [[ f ]]) (r 【 A , α , x 】) ≡ r 【 B , β , (G [[ f ]]) x 】
algHom【】 _ (ConstTerm x) = refl
algHom【】 _ 𝕩 = refl
algHom【】 {_} {H} {G} {_} {algebra A α} {algebra B β} {x} (algebraHom f h)
  (c i s) =
  (f $ scatter A H α i $ s 【 A , α , x 】)
    ≡⟨ funExt⁻ h (ink i $ s 【 A , α , x 】) ⟩
  β (( F-hom (⨁ H) f) (ink i (s 【 A , α , x 】)))
    ≡⟨ refl ⟩
  β (ink i ((H i [[ f ]]) (s 【 A , α , x 】)))
    ≡⟨ cong (scatter B H β i) (algHom【】 (algebraHom f h) s) ⟩
  scatter B H β i (s 【 B , β , (G [[ f ]]) x 】) ∎
algHom【】 f (π₁ r) = cong fst (algHom【】 f r)
algHom【】 f (π₂ r) = cong snd (algHom【】 f r)
algHom【】 f (r₁ , r₂) = ≡-× (algHom【】 f r₁) (algHom【】 f r₂)
algHom【】 f (in₁ r) = cong inl (algHom【】 f r)
algHom【】 f (in₂ r) = cong inr (algHom【】 f r)

polyFuncOnSet' : Sig 0 → Functor (SET ℓ-zero) (SET ℓ-zero)
polyFuncOnSet' = ⨁ ∘ snd ∘ fst 

Algebra' : Sig 0 → Type₁
Algebra' = Algebra ∘ polyFuncOnSet'

isLawful : ∀ S → Algebra' S → Type₀
isLawful ((k , H) , n , A , t , r) (algebra X α) =
   ∀ j x → t j 【 X , α , x 】 ≡ r j 【 X , α , x 】

LawfulSetAlgebra : Sig 0 → Type₁
LawfulSetAlgebra S = Σ (Algebra' S) (isLawful S)

isLawfulIsProp : ∀ S → (A : Algebra' S) → isProp (isLawful S A)
isLawfulIsProp _ (algebra (_ , k) _) = isOfHLevelΠ 1 λ _ →
                                       isOfHLevelΠ 1 λ _ → k _ _
AlgebrasCategory' : Sig 0 → Category (ℓ-suc ℓ-zero) ℓ-zero
AlgebrasCategory' = AlgebrasCategory ∘ polyFuncOnSet'

{-
Cubical Agda's standard library's "full subcategories" do not require
injectivity on objects, so we prove it separately as LawSetAlgIsInjOb.
-}
LawSetAlg : Sig 0 → Category (ℓ-suc ℓ-zero) ℓ-zero
LawSetAlg S = FullSubcategory (AlgebrasCategory' S) (isLawful S)

LawSetAlgIsInjOb : ∀ S → isEmbedding $ F-ob $
                         FullInclusion (AlgebrasCategory' S) (isLawful S)
LawSetAlgIsInjOb S = isEmbdIncl-ob (AlgebrasCategory' S) (isLawfulIsProp S)