gistfile1.txt

interleaved mutual
  data Sub  : Nat → Nat → Type
  data Term : Nat → Type

  private
    consS′ : ∀ {Δ Γ} → Sub Γ Δ → Term Γ → Sub Γ (suc Δ)
    _∘s′_  : ∀ {Γ Δ Θ} → Sub Δ Θ → Sub Γ Δ → Sub Γ Θ
    π₁′    : ∀ {Δ Γ} → Sub Δ (suc Γ) → Sub Δ Γ
    idS′   : ∀ {Γ} → Sub Γ Γ

  data Term where
    π₂   : ∀ {Γ Δ} → Sub Γ (suc Δ) → Term Γ
    lam  : ∀ {n}   → Term (suc n) → Term n
    app  : ∀ {n}   → Term n → Term (suc n)
    _[_] : ∀ {Δ Γ} → Term Δ → Sub Γ Δ → Term Γ

  data Sub where
    idS   : ∀ {Γ} → Sub Γ Γ
    _∘s_  : ∀ {Γ Δ Θ} → Sub Δ Θ → Sub Γ Δ → Sub Γ Θ
    consS : ∀ {Δ Γ} → Sub Γ Δ → Term Γ → Sub Γ (suc Δ)
    π₁    : ∀ {Δ Γ} → Sub Δ (suc Γ) → Sub Δ Γ
    εS    : ∀ {Γ} → Sub Γ 0

  data Term where
    π₂β    : ∀ {Γ Δ} (σ : Sub Γ Δ) {t : Term Γ} → π₂ (consS′ σ t) ≡ t
    β      : ∀ {Γ} (t : Term (suc Γ)) → app (lam t) ≡ t
    η      : ∀ {Γ} (t : Term Γ) → lam (app t) ≡ t
    λ[]    : ∀ {Γ Δ} (σ : Sub Δ Γ) (t : Term (suc Γ))
           → (lam t) [ σ ] ≡ lam (t [ consS′ (σ ∘s′ π₁′ idS′) (π₂ idS′) ])
    squash : ∀ {Γ} → is-set (Term Γ)

  data Sub where
    idlS : ∀ {Γ Δ} (σ : Sub Γ Δ) → idS ∘s σ ≡ σ
    idrS : ∀ {Γ Δ} (σ : Sub Γ Δ) → σ ∘s idS ≡ σ
    π₁β  : ∀ {Γ Δ} (σ : Sub Γ Δ) (t : Term Γ) → π₁ (consS σ t) ≡ σ
    πη   : ∀ {Γ Δ} (σ : Sub Γ (suc Δ)) → consS (π₁ σ) (π₂ σ) ≡ σ
    η0   : ∀ {Γ} (σ : Sub Γ 0) → σ ≡ εS
    assocS : ∀ {Γ Δ Θ Ι} (σ : Sub Θ Ι) (τ : Sub Δ Θ) (υ : Sub Γ Δ)
           → σ ∘s (τ ∘s υ) ≡ (σ ∘s τ) ∘s υ
    squash : ∀ {Γ Δ} → is-set (Sub Γ Δ)

  consS′ = consS
  _∘s′_ = _∘s_
  idS′ = idS
  π₁′ = π₁