{-# OPTIONS --type-in-type --rewriting #-}

infix 10 _≡_
infixl 30 _∷_
infixr 40 _⊚_
infixl 30 _▸_ _▹_
infix 60 _₀ _₁

data _≡_ {A : Set} (a : A) : A → Set where
  reflᵉ : a ≡ a

{-# BUILTIN REWRITE _≡_ #-}

data Tel : Set

el : Tel → Set

postulate
  _⇨_ : (Δ : Tel) (T : Set) → Set
  Λ⇨ : {Δ : Tel} {T : Set} → (el Δ → T) → (Δ ⇨ T)
  _⊘_ : {Δ : Tel} {T : Set} (B : Δ ⇨ T) (x : el Δ) → T
  ⊘β : {Δ : Tel} {T : Set} (B : el Δ → T) (x : el Δ) → (Λ⇨ {Δ} B) ⊘ x ≡ B x

{-# REWRITE ⊘β #-}

data _▹_ (Δ : Tel) (B : Δ ⇨ Set) : Set where
  _∷_ : (x : el Δ) → B ⊘ x → Δ ▹ B
open _▹_

data Tel where
  _▸_ : (Δ : Tel) (A : Δ ⇨ Set) → Tel

el (Δ ▸ A) = Δ ▹ A

pop : {Δ : Tel} {B : Δ ⇨ Set} → Δ ▹ B → el Δ
pop (δ ∷ _) = δ

top : {Δ : Tel} {B : Δ ⇨ Set} (δ : Δ ▹ B) → B ⊘ (pop δ)
top (_ ∷ b) = b

postulate
  _⊚_ : {Γ Δ : Tel} {T : Set} (g : Δ ⇨ T) (f : Γ ⇨ el Δ) → (Γ ⇨ T)
  ⊚⊘ : {Γ Δ : Tel} {T : Set} (g : Δ ⇨ T) (f : Γ ⇨ el Δ) (x : el Γ) →
    (g ⊚ f) ⊘ x ≡ g ⊘ (f ⊘ x)

{-# REWRITE ⊚⊘ #-}

ID : Tel → Tel

_₀ : {Δ : Tel} → el (ID Δ) → el Δ
_₁ : {Δ : Tel} → el (ID Δ) → el Δ

Λ₀ : {Δ : Tel} → (ID Δ) ⇨ el Δ
Λ₀ = (Λ⇨ λ x → x ₀)

Λ₁ : {Δ : Tel} → (ID Δ) ⇨ el Δ
Λ₁ = (Λ⇨ λ x → x ₁)

postulate
  Id : {Δ : Tel} (A : Δ ⇨ Set) (δ : el (ID Δ)) (a₀ : A ⊘ (δ ₀)) (a₁ : A ⊘ (δ ₁)) → Set

ID▸▸ : {Δ : Tel} (A : Δ ⇨ Set) → Tel
ID▸▸ {Δ} A = ID Δ ▸ (A ⊚ Λ₀) ▸ (A ⊚ Λ₁ ⊚ (Λ⇨ λ x → pop x))

Id/ : {Δ : Tel} (A : Δ ⇨ Set) → ID▸▸ A ⇨ Set
Id/ A = (Λ⇨ λ x → Id A (pop (pop x)) (top (pop x)) (top x))

ID (Δ ▸ A) = ID▸▸ A ▸ Id/ A

_₀ {Δ ▸ A} (δ ∷ a₀ ∷ a₁ ∷ a₂) = δ ₀ ∷ a₀

_₁ {Δ ▸ A} (δ ∷ a₀ ∷ a₁ ∷ a₂) = δ ₁ ∷ a₁

postulate
  AP : {Γ Δ : Tel} (f : Γ ⇨ el Δ) (γ : el (ID Γ)) → el (ID Δ)
  AP₀ : {Γ Δ : Tel} (f : Γ ⇨ el Δ) (γ : el (ID Γ)) → (AP f γ)₀ ≡ f ⊘ (γ ₀)
  AP₁ : {Γ Δ : Tel} (f : Γ ⇨ el Δ) (γ : el (ID Γ)) → (AP f γ)₁ ≡ f ⊘ (γ ₁)

{-# REWRITE AP₀ AP₁ #-}

postulate
  Id-AP⊚ : {Γ Δ : Tel} (f : Γ ⇨ el Δ) (γ : el (ID Γ)) (A : Δ ⇨ Set)
          (a₀ : A ⊘ (f ⊘ (γ ₀))) (a₁ : A ⊘ (f ⊘ (γ ₁))) →
    Id (A ⊚ f) γ a₀ a₁ ≡ Id A (AP f γ) a₀ a₁

{-# REWRITE Id-AP⊚ #-}

SQ : Tel → Tel
SQ Δ = ID (ID Δ)

module Square
  {Δ : Tel} (A : Δ ⇨ Set) (δ : el (SQ Δ))
  {a₀₀ : A ⊘ (δ ₀ ₀)} {a₀₁ : A ⊘ (δ ₁ ₀)} (a₀₂ : Id A (AP Λ₀ δ) a₀₀ a₀₁)
  {a₁₀ : A ⊘ (δ ₀ ₁)} {a₁₁ : A ⊘ (δ ₁ ₁)} (a₁₂ : Id A (AP Λ₁ δ) a₁₀ a₁₁)
  (a₂₀ : Id A (δ ₀) a₀₀ a₁₀) (a₂₁ : Id A (δ ₁) a₀₁ a₁₁) where

  Sq : Set
  Sq = Id {ID▸▸ A} (Id/ A) (δ ∷ a₀₀ ∷ a₀₁ ∷ a₀₂ ∷ a₁₀ ∷ a₁₁ ∷ {!a₁₂!}) a₂₀ a₂₁

  sq∷ : (a₂₂ : Sq) → el (SQ (Δ ▸ A))
  sq∷ a₂₂ = δ ∷ a₀₀ ∷ a₀₁ ∷ a₀₂ ∷ a₁₀ ∷ a₁₁ ∷ {!a₁₂!} ∷ a₂₀ ∷ a₂₁ ∷ a₂₂

  postulate
    sq∷₀₂ : (a₂₂ : Sq) → AP (Λ₀ {Δ ▸ A}) (sq∷ a₂₂) ≡ (AP Λ₀ δ) ∷ a₀₀ ∷ a₀₁ ∷ a₀₂

  {-# REWRITE sq∷₀₂ #-}