module ImprHIT.SetTruncated.Rules where

open import Cubical.Categories.Functor
open import Cubical.Categories.Instances.Sets
open import Cubical.Categories.Instances.FunctorAlgebras
open import Cubical.Data.FinData.Base
open import Cubical.Data.Sigma.Properties
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Path
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 import ImprHIT.SetTruncated.Initial

open Algebra
open AlgebraHom
open Functor
open Iso
open FinSum

TypeEncoding : Sig  → Type₀
TypeEncoding = fst ∘ InitialLawSetAlgebraCarrier

TypeIsSetEncoding : ∀ S → isSet (TypeEncoding S)
TypeIsSetEncoding = snd ∘ InitialLawSetAlgebraCarrier

PointConstrEncoding : (S@((k , H) , _ ) : Sig ) → (i : Fin k) →
                      fst ((H i) [ InitialLawSetAlgebraCarrier S ]) →
                      TypeEncoding S
PointConstrEncoding S@((_ , H) , _) = scatter (InitialLawSetAlgebraCarrier S) H
  $ str $ fst $ fst $ InitialLawSetAlg S

ClusterScatterPointConstrEncoding : (S@((_ , H) , _ , _ , t , r) : Sig ) →
  let X = InitialLawSetAlgebraCarrier S
  in cluster (InitialLawSetAlgebraCarrier S) H (PointConstrEncoding S)
     ≡ (str $ fst $ fst $ InitialLawSetAlg S)
ClusterScatterPointConstrEncoding S@((_ , H) , _) =
  let X = InitialLawSetAlgebraCarrier S
  in leftInv (scatterIso X H) $ str $ fst $ fst $ InitialLawSetAlg S

PathConstrEncoding : (S@((_ , H) , _ , _ , t , r) : Sig ) →
  let X = InitialLawSetAlgebraCarrier S
      α = cluster (InitialLawSetAlgebraCarrier S) H (PointConstrEncoding S)
  in ∀ j x → t j 【 X , α , x 】 ≡ r j 【 X , α , x 】
PathConstrEncoding S@((_ , H) , _ , _ , t , r) =
  let X = InitialLawSetAlgebraCarrier S
      α = cluster (InitialLawSetAlgebraCarrier S) H (PointConstrEncoding S)
  in subst (λ α → ∀ j x → (t j 【 X , α , x 】) ≡ (r j 【 X , α , x 】))
     (sym $ ClusterScatterPointConstrEncoding S)
     $ snd $ fst $ InitialLawSetAlg S

RecEncoding : (S@((_ , H) , _ , _ , t , r) : Sig ) →
              (X@(X₀ , hX) : hSet ℓ-zero) →
              (d : ∀ i → fst (H i [ X ]) → X₀) →
              (∀ j x →
                (t j)【 X , cluster X H d , x 】 ≡
                (r j)【 X , cluster X H d , x 】) →
              TypeEncoding S → X₀
RecEncoding ((_ , H) , _) X d q s =
  ev (fst s) $ algebra X (cluster X H d) , q

βEncoding : (S@((_ , H) , _ , _ , t , r) : Sig ) →
              (X@(X₀ , hX) : hSet ℓ-zero) →
              (d : ∀ i → fst (H i [ X ]) → X₀) →
              (q : ∀ j x →
                (t j)【 X , cluster X H d , x 】 ≡
                (r j)【 X , cluster X H d , x 】) →
            ∀ i x →
            RecEncoding S X d q (PointConstrEncoding S i x) ≡
            d i ((H i [[ RecEncoding S X d q ]]) x)
βEncoding S@((_ , H) , _) X d q i x =
  RecEncoding S X d q (PointConstrEncoding S i x)
    ≡⟨ refl ⟩
  d i ((H i [[ RecEncoding S X d q ]]) x) ∎

weakηEncoding : ∀ S → RecEncoding S (InitialLawSetAlgebraCarrier S)
                (PointConstrEncoding S) (PathConstrEncoding S) ≡ idfun _
weakηEncoding S@((_ , H) , _) = funExt λ x@(ϕ , φ) →
  ΣPathPProp (natIsProp $ ForgetLawSetAlg S ∘F 𝟙⟨ LawSetAlg S ⟩) $
  funExtImpr λ 𝔹@(algebra B β , h) →
  let I@((algebra I₀ α₀) , p₀) = fst (InitialLawSetAlg S)
      clusterScatterβ = leftInv (scatterIso B H) β
      𝔹' = algebra B (cluster B H $ scatter B H β) ,
           subst (isLawful S ∘ algebra B) (sym clusterScatterβ) h
      𝔹'is𝔹 : 𝔹' ≡ 𝔹
      𝔹'is𝔹 = ΣPathP $ cong (λ x → algebra {F = ⨁ H} B x) clusterScatterβ ,
              λ i → subst-filler (isLawful S ∘ algebra B)
              (λ i → clusterScatterβ (~ i)) h (~ i)
  in
    ev (fst $ RecEncoding S I₀ (PointConstrEncoding S)
    (PathConstrEncoding S) x) 𝔹
      ≡⟨ cong (ev (fst $ RecEncoding S I₀ (PointConstrEncoding S)
         (PathConstrEncoding S) x)) (sym 𝔹'is𝔹) ⟩
    ev (fst $ RecEncoding S I₀ (PointConstrEncoding S)
    (PathConstrEncoding S) x) 𝔹'
      ≡⟨ refl ⟩
    ev (fst $ ev ϕ $ algebra I₀ (cluster I₀ H $ PointConstrEncoding S) ,
    PathConstrEncoding S) 𝔹'
      ≡⟨ cong₂ (λ x y → ev (fst $ ev ϕ $ algebra I₀ x , y) 𝔹')
         (ClusterScatterPointConstrEncoding S)
         $ fst $ isProp→isContrPathP
           (λ i → isLawfulIsProp S $ algebra I₀ $
           ClusterScatterPointConstrEncoding S i) _ _ ⟩
    ev (fst $ ev ϕ $ algebra I₀ α₀ , p₀) 𝔹'
      ≡⟨ refl ⟩
    ev (fst $ ev ϕ I) 𝔹'
      ≡⟨ cong (ev $ fst $ ev ϕ I) 𝔹'is𝔹 ⟩
    ev (fst $ ev ϕ I) 𝔹
      ≡⟨ ev (ev (ev φ I) 𝔹) $ fst $ (snd $ InitialLawSetAlg S) 𝔹 ⟩
    ev ϕ 𝔹 ∎

ηEncoding : ∀ (S@((_ , H) , _ , _ , t , r) : Sig )
              (X@(X₀ , hX) : hSet ℓ-zero)
              (d : ∀ i → fst (H i [ X ]) → X₀)
              (q : ∀ j x → (t j)【 X , cluster X H d , x 】 ≡
                           (r j)【 X , cluster X H d , x 】)
              (f : TypeEncoding S → X₀) →
              f ∘ (cluster _ H $ PointConstrEncoding S) ≡
              cluster X H d ∘ F-hom (⨁ H) f → RecEncoding S X d q ≡ f
ηEncoding S@((_ , H) , _) X d q f h = funExt λ x →
  let I@((algebra I₀ α₀) , p₀) = fst (InitialLawSetAlg S) in
    RecEncoding S X d q x
      ≡⟨ refl ⟩
    ev (fst x) (algebra X (cluster X H d) , q)
      ≡⟨ sym $ ev (ev (ev (snd x) $ algebra I₀ (cluster I₀ H $
         PointConstrEncoding S) , PathConstrEncoding S) $ algebra X
         (cluster X H d) , q) $ algebraHom f h ⟩
    f (ev (fst x) $
      algebra I₀ (cluster I₀ H $ PointConstrEncoding S) , PathConstrEncoding S)
      ≡⟨ refl ⟩
    f (RecEncoding S I₀ (PointConstrEncoding S) (PathConstrEncoding S) x)
      ≡⟨ cong f $ funExt⁻ (weakηEncoding S) x ⟩
    f x ∎