module ImprHIT.Background.Weide where

open import Agda.Builtin.Cubical.Equiv
open import Cubical.Categories.Functor
open import Cubical.Categories.Instances.Sets
open import Cubical.Data.Empty
open import Cubical.Data.FinData
open import Cubical.Data.Nat
open import Cubical.Data.Sigma
open import Cubical.Data.Sum
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Prelude

open Functor

private
  variable
    ℓ : Level
    h : HLevel
    A : Type ℓ
    B : A → Type ℓ

data PolyTypeConstr (ℓ : Level) (h : HLevel) : Type (ℓ-suc ℓ) where
  Const : TypeOfHLevel ℓ (2 + h) → PolyTypeConstr ℓ h
  𝕏     : PolyTypeConstr ℓ h
  _⊗_   : PolyTypeConstr ℓ h → PolyTypeConstr ℓ h → PolyTypeConstr ℓ h
  _⊕_   : PolyTypeConstr ℓ h → PolyTypeConstr ℓ h → PolyTypeConstr ℓ h

_[_] : PolyTypeConstr ℓ h →
       TypeOfHLevel ℓ (2 + h) → TypeOfHLevel ℓ (2 + h)
Const A [ _ ] = A
𝕏 [ B ] = B
_[_] {h = h} (F ⊗ G) B = let (X , k) = F [ B ]
                             (Y , l) = G [ B ]
                         in X × Y , isOfHLevel× (2 + h) k l
_[_] {h = h} (F ⊕ G) B = let (X , k) = F [ B ]
                             (Y , l) = G [ B ]
                         in (X ⊎ Y) , isOfHLevel⊎ h k l

_[[_]] : {(B , k) (C , l) : TypeOfHLevel ℓ (2 + h)}
  (F : PolyTypeConstr ℓ h) → (B → C) → fst (F [ B , k ]) → fst (F [ C , l ])
Const (A , _) [[ _ ]] = idfun A
𝕏 [[ f ]]       = f
(F ⊗ G) [[ f ]] = map-× (F [[ f ]]) (G [[ f ]])
(F ⊕ G) [[ f ]] = map (F [[ f ]]) (G [[ f ]])

polyFuncOnSet : PolyTypeConstr ℓ 0 → Functor (SET ℓ) (SET ℓ)
polyFuncOnSet F = record {
  F-ob = F [_] ;
  F-hom = F [[_]] ;
  F-id = eval-id F ;
  F-seq = eval-seq F }
  where 
  eval-id : (F : PolyTypeConstr ℓ h) {(X , k) : TypeOfHLevel ℓ (2 + h)} →
    F [[ idfun X ]] ≡ idfun (fst (F [ X , k ]))
  eval-id (Const _) = refl
  eval-id 𝕏         = refl
  eval-id (F ⊗ G)   = cong₂ map-× (eval-id F) (eval-id G)
  eval-id (F ⊕ G)   = funExt λ {
    (inl z) → cong inl $ funExt⁻ (eval-id F) z ;
    (inr z) → cong inr $ funExt⁻ (eval-id G) z }
  eval-seq : (F : PolyTypeConstr ℓ h)
    {(X , k) (Y , l) (Z , m) : TypeOfHLevel ℓ (2 + h)}
    (f : X → Y) (g : Y → Z) →
    _[[_]] {ℓ} {h} {_} {(Z , m)} F (g ∘ f) ≡
    F [[ g ]] ∘ (_[[_]] {ℓ} {h} {(X , k)} {(Y , l)} F f) 
  eval-seq (Const x) _ _ = refl
  eval-seq 𝕏 _ _ = refl
  eval-seq (F ⊗ G) f g = cong₂ map-× (eval-seq F f g) (eval-seq G f g)
  eval-seq (F ⊕ G) f g = funExt λ {
    (inl a) → cong inl $ funExt⁻ (eval-seq F f g) a ;
    (inr a) → cong inr $ funExt⁻ (eval-seq G f g) a }

private
  variable
    k : ℕ

module FinSum where

  private
    variable
      H : Fin k → Type ℓ

  data FinSum (H : Fin k → Type ℓ) : Type ℓ where
    ink : (i : Fin k) → H i → FinSum H

  FinSumFst : {H : Fin k → Type ℓ} (x : FinSum H) → Fin k
  FinSumFst (ink i _) = i

  FinSumSnd : (x : FinSum H) → H (FinSumFst x)
  FinSumSnd (ink _ x) = x

  ≡FinSum : {x y : FinSum H} (p : x ≡ y) →
          Σ (FinSumFst x ≡ FinSumFst y)
          λ q → PathP (λ i → congS H q i) (FinSumSnd x) (FinSumSnd y)
  ≡FinSum {x = ink i a} {y = ink j b} p = cong FinSumFst p , cong FinSumSnd p
   
  isOfHLevelSuc⊥ : ∀ h → isOfHLevel {ℓ} (suc h) ⊥*
  isOfHLevelSuc⊥ h = isProp→isOfHLevelSuc h isProp⊥*

  FinSum' : (Fin k → Type ℓ) → Type ℓ
  FinSum' {ℓ} {h} = foldrFin (_⊎_) ⊥*

  isOfHLevelFinSum' : ∀ h (H : Fin k → TypeOfHLevel ℓ (2 + h)) →
                   isOfHLevel (2 + h) (FinSum' (fst ∘ H))
  isOfHLevelFinSum' {0} h H = isOfHLevelSuc⊥ (suc h)
  isOfHLevelFinSum' {suc n} h H = isOfHLevel⊎ h (snd $ H zero)
                                  (isOfHLevelFinSum' h $ H ∘ suc)

  FinSumToFinSum' : (H : Fin k → Type ℓ) → FinSum H → FinSum' H
  FinSumToFinSum' H (ink zero x) = inl x
  FinSumToFinSum' H (ink (suc i) x) = inr $ FinSumToFinSum' (H ∘ suc) $ ink i x

  FinSum'ToFinSum : (H : Fin k → Type ℓ) → FinSum' H → FinSum H
  FinSum'ToFinSum {k = 0} _ ()
  FinSum'ToFinSum {k = suc i} H (inl x) = ink Fin.zero x
  FinSum'ToFinSum {k = suc i} H (inr x) with FinSum'ToFinSum (H ∘ suc) x
  ...                                      | ink j y = ink (Fin.suc j) y

  FinSum'ToFinSumIsRetract : (H : Fin k → Type ℓ) → (x : FinSum H) →
                         FinSum'ToFinSum H (FinSumToFinSum' H x) ≡ x
  FinSum'ToFinSumIsRetract {k = 0} _ (ink i _) =
    Cubical.Data.Empty.rec (¬Fin0 i)
  FinSum'ToFinSumIsRetract {k = suc _} _ (ink zero _) = refl
  FinSum'ToFinSumIsRetract {k = suc i} H (ink (suc j) x)
    with FinSum'ToFinSumIsRetract (H ∘ suc) (ink j x)
  ...  | p with FinSum'ToFinSum (H ∘ suc) $ FinSumToFinSum' (H ∘ suc) (ink j x)
  ...         | ink h y =
                  let (α , β) = ≡FinSum p
                  in cong₂ ink (cong Fin.suc α) β

  isOfHLevelFinSum : ∀ h (H : Fin k → TypeOfHLevel ℓ (2 + h)) →
                   isOfHLevel (2 + h) (FinSum (fst ∘ H))
  isOfHLevelFinSum h H = isOfHLevelRetract (2 + h)
    (FinSumToFinSum' $ fst ∘ H)
    (FinSum'ToFinSum $ fst ∘ H)
    (FinSum'ToFinSumIsRetract $ fst ∘ H)
    (isOfHLevelFinSum' h H)

open FinSum

⨁ : (H : Fin k → PolyTypeConstr ℓ 0) → Functor (SET ℓ) (SET ℓ)
⨁ H = record {
  F-ob = λ X → FinSum (fst ∘ ((_[ X ]) ∘ H)) , isOfHLevelFinSum 0 (_[ X ] ∘ H) ;
  F-hom = λ f → λ { (ink i x) → ink i ((H i [[ f ]]) x) } ;
  F-id = funExt λ { (ink i x) →
         cong (ink i) $ funExt⁻ (F-id (polyFuncOnSet (H i))) x } ;
  F-seq = λ f g → funExt λ { (ink i x) →
          cong (ink i) $ funExt⁻ (F-seq (polyFuncOnSet (H i)) f g) x } }

scatter : ∀ X (H : Fin k → PolyTypeConstr ℓ 0) →
          (fst (F-ob (⨁ H) X) → fst X) → (i : Fin k) → fst (H i [ X ]) → fst X
scatter _ _ α i = α ∘ ink i

cluster : ∀ X (H : Fin k → PolyTypeConstr ℓ 0) →
          ((i : Fin k) → fst (H i [ X ]) → fst X) → fst (F-ob (⨁ H) X) → fst X
cluster _ _ d (ink i x) = d i x

scatterIso : ∀ X (H : Fin k → PolyTypeConstr ℓ 0) →
           Iso (fst (F-ob (⨁ H) X) → fst X) ((i : Fin k) → fst (H i [ X ]) → fst X)
scatterIso X H = iso (scatter X H) (cluster X H)
  (λ _ → funExt λ _ → funExt λ _ → refl )
  (λ _ → funExt λ { (ink _ _) → refl } )

scatterEquiv : ∀ X (H : Fin k → PolyTypeConstr ℓ 0) →
           (fst (F-ob (⨁ H) X) → fst X) ≃ ((i : Fin k) → fst (H i [ X ]) → fst X)
scatterEquiv X H = isoToEquiv (scatterIso X H)

data PathConstructorTerm
  (H : Fin k → PolyTypeConstr ℓ h) (F : PolyTypeConstr ℓ h) :
  PolyTypeConstr ℓ h → Type (ℓ-suc ℓ) where
  ConstTerm : ∀ {A} → fst A → PathConstructorTerm H F (Const A)
  𝕩         : PathConstructorTerm H F F
  c         : ∀ i → PathConstructorTerm H F (H i) → PathConstructorTerm H F 𝕏
  π₁        : ∀ {G₁ G₂} → PathConstructorTerm H F (G₁ ⊗ G₂) →
              PathConstructorTerm H F G₁
  π₂        : ∀ {G₁ G₂} → PathConstructorTerm H F (G₁ ⊗ G₂) →
              PathConstructorTerm H F G₂
  _,_       : ∀ {G₁ G₂} → PathConstructorTerm H F G₁ →
              PathConstructorTerm H F G₂ → PathConstructorTerm H F (G₁ ⊗ G₂)
  in₁       : ∀ {G₁ G₂} → PathConstructorTerm H F G₁ →
              PathConstructorTerm H F (G₁ ⊕ G₂)
  in₂       : ∀ {G₁ G₂} → PathConstructorTerm H F G₂ →
              PathConstructorTerm H F (G₁ ⊕ G₂)

_【_,_,_】 : ∀ {H : Fin k → PolyTypeConstr ℓ 0}
       {F G} → PathConstructorTerm H F G → (B : TypeOfHLevel ℓ 2)
       (d : fst (F-ob (⨁ H) B) → fst B) → fst (F [ B ]) → fst (G [ B ])
ConstTerm a 【 _ , _ , _ 】 = a
_【_,_,_】 𝕩 B _ = idfun _
_【_,_,_】 {H = H} (c i s) B d y = scatter B H d i (s 【 B , d , y 】)
π₁ s 【 B , d , y 】 = fst (s 【 B , d , y 】)
π₂ s 【 B , d , y 】 = snd (s 【 B , d , y 】)
(s , t) 【 B , d , y 】 = s 【 B , d , y 】 , t 【 B , d , y 】
in₁ s 【 B , d , y 】 = inl (s 【 B , d , y 】)
in₂ s 【 B , d , y 】 = inr (s 【 B , d , y 】)

PointConstructors : HLevel → Type (ℓ-suc ℓ)
PointConstructors {ℓ} h = Σ ℕ λ k → Fin k → PolyTypeConstr ℓ h

PathConstructors : PointConstructors h → Type (ℓ-suc ℓ)
PathConstructors {h} {ℓ} (k , H) =
  Σ ℕ λ n →                                     -- number of path constructors
  Σ (Fin n → PolyTypeConstr ℓ h) λ A →          -- polynomial path arguments
  Σ (∀ j → PathConstructorTerm H (A j) 𝕏) λ t → -- left endpoints
     ∀ j → PathConstructorTerm H (A j) 𝕏        -- right endpoints

Sig : HLevel → Type (ℓ-suc ℓ)
Sig h = Σ (PointConstructors h) PathConstructors