open import Cubical.Foundations.Prelude hiding (Sub)
open import Cubical.Foundations.HLevels

module TT.Wild.Examples (X : hSet ℓ-zero) (Y : X .fst → hSet ℓ-zero) where

open import TT.Wild.Syntax X Y

private variable
  Γ Δ : Con
  A B : Ty Γ

[]ᵀ-⟨⟩-∘ :
  (B : Ty (Γ ▹ A)) (a : Tm Γ A) (γ : Sub Δ Γ) →
  B [ ⟨ a ⟩ ]ᵀ [ γ ]ᵀ ≡ B [ γ ⁺ ]ᵀ [ ⟨ a [ γ ]ᵗ ⟩ ]ᵀ
[]ᵀ-⟨⟩-∘ {Δ} B a γ = λ i → filler i1 i
  module []ᵀ-⟨⟩-∘ where
  filler : (j i : I) → Ty Δ
  filler j i =
    hfill
      (λ where
        j (i = i0) → []ᵀ-∘ B ⟨ a ⟩ γ j
        j (i = i1) → []ᵀ-∘ B (γ ⁺) ⟨ a [ γ ]ᵗ ⟩ j)
      (inS (B [ ⟨⟩-∘ a γ i ]ᵀ))
      j

[]ᵗ-⟨⟩-∘ :
  (b : Tm (Γ ▹ A) B) (a : Tm Γ A) (γ : Sub Δ Γ) →
  PathP (λ i → Tm Δ ([]ᵀ-⟨⟩-∘ B a γ i))
    (b [ ⟨ a ⟩ ]ᵗ [ γ ]ᵗ)
    (b [ γ ⁺ ]ᵗ [ ⟨ a [ γ ]ᵗ ⟩ ]ᵗ)
[]ᵗ-⟨⟩-∘ {B} {Δ} b a γ i =
  comp (λ j → Tm Δ ([]ᵀ-⟨⟩-∘.filler B a γ j i))
    (λ where
      j (i = i0) → []ᵗ-∘ b ⟨ a ⟩ γ j
      j (i = i1) → []ᵗ-∘ b (γ ⁺) ⟨ a [ γ ]ᵗ ⟩ j)
    (b [ ⟨⟩-∘ a γ i ]ᵗ)

[]ᵀ-▹-η : (B : Ty (Γ ▹ A)) → B ≡ B [ p ⁺ ]ᵀ [ ⟨ q ⟩ ]ᵀ
[]ᵀ-▹-η {Γ} {A} B = λ i → filler i1 i
  module []ᵀ-▹-η where
  filler : (j i : I) → Ty (Γ ▹ A)
  filler j i =
    hfill
      (λ where
        j (i = i0) → []ᵀ-id B j
        j (i = i1) → []ᵀ-∘ B (p ⁺) ⟨ q ⟩ j)
      (inS (B [ ▹-η i ]ᵀ))
      j

[]ᵗ-▹-η :
  (b : Tm (Γ ▹ A) B) →
  PathP (λ i → Tm (Γ ▹ A) ([]ᵀ-▹-η B i)) b (b [ p ⁺ ]ᵗ [ ⟨ q ⟩ ]ᵗ)
[]ᵗ-▹-η {Γ} {A} {B} b i =
  comp (λ j → Tm (Γ ▹ A) ([]ᵀ-▹-η.filler B j i))
    (λ where
      j (i = i0) → []ᵗ-id b j
      j (i = i1) → []ᵗ-∘ b (p ⁺) ⟨ q ⟩ j)
    (b [ ▹-η i ]ᵗ)

infixl  _[_]ᵖ
_[_]ᵖ : Tm Γ (Π A B) → (γ : Sub Δ Γ) → Tm Δ (Π (A [ γ ]ᵀ) (B [ γ ⁺ ]ᵀ))
_[_]ᵖ {A} {B} {Δ} f γ = filler i1
  module []ᵖ where
  filler : (i : I) → Tm Δ (Π-[] A B γ i)
  filler i = transport-filler (λ i → Tm Δ (Π-[] A B γ i)) (f [ γ ]ᵗ) i

lam-[]ᵖ : (b : Tm (Γ ▹ A) B) (γ : Sub Δ Γ) → lam b [ γ ]ᵖ ≡ lam (b [ γ ⁺ ]ᵗ)
lam-[]ᵖ b γ = fromPathP (lam-[] b γ)

app-[] : (f : Tm Γ (Π A B)) (γ : Sub Δ Γ) → app f [ γ ⁺ ]ᵗ ≡ app (f [ γ ]ᵖ)
app-[] f γ =
  sym (Π-β (app f [ γ ⁺ ]ᵗ)) ∙
  cong app (sym (lam-[]ᵖ (app f) γ) ∙ cong _[ γ ]ᵖ (sym (Π-η f)))

infixl  _·_
_·_ : Tm Γ (Π A B) → (a : Tm Γ A) → Tm Γ (B [ ⟨ a ⟩ ]ᵀ)
f · a = app f [ ⟨ a ⟩ ]ᵗ

·-[] :
  (f : Tm Γ (Π A B)) (a : Tm Γ A) (γ : Sub Δ Γ) →
  PathP (λ i → Tm Δ ([]ᵀ-⟨⟩-∘ B a γ i))
    ((f · a) [ γ ]ᵗ)
    ((f [ γ ]ᵖ) · (a [ γ ]ᵗ))
·-[] f a γ = []ᵗ-⟨⟩-∘ (app f) a γ ▷ cong _[ ⟨ a [ γ ]ᵗ ⟩ ]ᵗ (app-[] f γ)

Π-β′ : (b : Tm (Γ ▹ A) B) (a : Tm Γ A) → lam b · a ≡ b [ ⟨ a ⟩ ]ᵗ
Π-β′ b a = cong _[ ⟨ a ⟩ ]ᵗ (Π-β b)

Π-η′ :
  (f : Tm Γ (Π A B)) →
  PathP (λ i → Tm Γ (Π A ([]ᵀ-▹-η B i))) f (lam ((f [ p ]ᵖ) · q))
Π-η′ f i =
  hcomp
   (λ where
     j (i = i0) → Π-η f (~ j)
     j (i = i1) → lam (app-[] f p j [ ⟨ q ⟩ ]ᵗ))
   (lam ([]ᵗ-▹-η (app f) i))