Chuangjie Xu & Martin Escardo, 7th March 2014

Type theory eating itself?
--------------------------

This is based on Coquand's presentation of the syntax of type theory
and its semantics in set theory using families (pdf version sent to
the HoTT list 20 Feb 2014).

We also incorporate a treatment of a tower of universes by Coquand,
Escardo & Spitters (2013 at IAS), using "Type n" judgements with
corresponding universes U n, interpreted as Set n, where Set n is the
nth Grothendieck universe.

Some differences:

 (0) We use type theory for the semantics, rather than set theory, and
     hence type theoretic universes.

 (1) We don't have judgemental equality in our type theory.
     But the required equations hold in the model, *judgementally*. 

     We instead have syntactic "transport" functions "T" presented as
     term constructors.

     Conjecture: this theory has the same expressivity as the theory
     with judgemental equality.

 (2) We modify the treatment of universes so that our syntax can be
     directly interpreted in Agda (which in particular lacks
     cumulativity).

     We use Agda's universe levels, which should be regarded as
     natural numbers in the meta-language (outside Agda), ranged over
     by i,j,k. Definitions with levels should be regarded as
     schematic, even though Agda does allow quantification over
     levels. So if a definition has a level i as a parameter, it
     should be considered as countably many definitions, with
     i=0,1,2,..., of which only finitely many levels are invoked in
     each use.

Also, although we have El and |-| in the syntax, they are identity
functions in the semantics, so that we have universes à la Russell
(because Agda's Set-universes are à la Russell).

This file typechecks in Agda version 2.3.3.
http://www.cs.bham.ac.uk/~mhe/TT-perhaps-eating-itself/TT-perhaps-eating-itself.lagda

\begin{code}

module TT-perhaps-eating-itself where

open import Agda.Primitive using (Level ; lzero ; lsuc ; _⊔_)
open import Preliminaries

\end{code}

Syntax. This follows closely Coquand's approach, with the differences
discussed above.

We have, as usual, contexts, substitutions, types and terms:

\begin{code}

data Cxt   : Level               → Set
data Subst : {i j : Level}       → Cxt i → Cxt j → Set
data Type  : {i : Level} → Level → Cxt i → Set
data Term  : {i j : Level}       → (Γ : Cxt i) → Type j Γ → Set

\end{code}

These are mutually recursively defined below.

For contexts, we have:

  ε      the empty context,
  Γ·A    the extension of the context Γ with the type A.

\begin{code}

data Cxt where
  ε   : {i : Level} → Cxt i
  _·_ : {i j : Level} (Γ : Cxt i) → Type j Γ → Cxt(i ⊔ j)

\end{code}

For types, we have:

  A[σ]        the application of the substitution σ to the type A,
  Sigma, Pi   dependent sum and product,
  U j         the jth universe, in any context of level i, which has type j+1,
  El u        the type corresponding to the term u:U.

\begin{code}

data Type where
  _[_]  : {i j k : Level} {Γ : Cxt i} {Δ : Cxt j} → Type k Γ → Subst Δ Γ → Type k Δ
  Sigma : {i j k : Level} {Γ : Cxt i} (A : Type j Γ) → Type k (Γ · A) → Type (j ⊔ k) Γ
  Pi    : {i j k : Level} {Γ : Cxt i} (A : Type j Γ) → Type k (Γ · A) → Type (j ⊔ k) Γ
  U     : {i : Level} {Γ : Cxt i} (j : Level) → Type (lsuc j) Γ
  El    : {i j : Level} {Γ : Cxt i} → Term Γ (U j) → Type j Γ

\end{code}

For substitutions, we have
  
  I       the identity,
  σ◦τ     the composition of the substitutions σ and τ,
  p       the (first-)projection substitution,
  ₍σ,u₎   extension.

\begin{code}

data Subst where
  I     : {i : Level} {Γ : Cxt i} → Subst Γ Γ
  _◦_   : {i j k : Level} {Γ : Cxt i} {Δ : Cxt j} {Ξ : Cxt k} → Subst Δ Γ → Subst Ξ Δ → Subst Ξ Γ
  p     : {i j : Level} {Γ : Cxt i} {A : Type j Γ} → Subst (Γ · A) Γ
  ₍_,_₎ : {i j k : Level} {Γ : Cxt i} {Δ : Cxt j} {A : Type k Γ}
          (σ : Subst Δ Γ) → Term Δ (A [ σ ]) → Subst Δ (Γ · A)

\end{code}

The following functions are "macros", used for clarity. Technically,
they are mutually recursively defined together with contexts, types,
terms, substitutions. We could have simply expanded their definitions
below, at the expense of making the definitions of term constructors
more unreadable (and this is what our first version of the definition
was).

They are the substitutions

  B ⌜ u ⌝ := B [ ₍ I , u ₎ ],
  v ⌞ u ⌟ := v ⟨ ₍ I , u ₎ ⟩, 
  B ⌈ σ ⌉ := B [ ₍ σ ◦ p , q ₎ ], 
  u ⌊ σ ⌋ := u ⟨ ₍ σ ◦ p , q ₎ ⟩.

However, because we don't have judgemental equality in our theory, we
need to apply syntactic transport functions at appropriate places:

  B ⌜ u ⌝ := B [ ₍ I , T₁ u ₎ ],
  v ⌞ u ⌟ := v ⟨ ₍ I , T₁ u ₎ ⟩, 
  B ⌈ σ ⌉ := B [ ₍ σ ◦ p , T₀ q ₎ ], 
  u ⌊ σ ⌋ := u ⟨ ₍ σ ◦ p , T₀ q ₎ ⟩.

We are not able to define these functions at this point, because T₀
and T₁ haven't been defined (they are term constructors below). We
just declare their type, so that the definition of terms can use it:

\begin{code}

_⌜_⌝ : {i j k : Level} {Γ : Cxt i} {A : Type j Γ} →
       Type k (Γ · A) → Term Γ A → Type k Γ

_⌞_⌟ : {i j k : Level} {Γ : Cxt i} {A : Type j Γ} {B : Type k (Γ · A)} →
       Term (Γ · A) B → (u : Term Γ A) → Term Γ (B ⌜ u ⌝)

_⌈_⌉ : {i j k l : Level} {Γ : Cxt i} {Δ : Cxt j} {A : Type k Γ} →
       Type l (Γ · A) → (σ : Subst Δ Γ) → Type l (Δ · (A [ σ ]))

_⌊_⌋ : {i j k l : Level} {Γ : Cxt i} {Δ : Cxt j} {A : Type k Γ} {B : Type l (Γ · A)} →
       Term (Γ · A) B → (σ : Subst Δ Γ) → Term (Δ · (A [ σ ])) (B ⌈ σ ⌉)

\end{code}

For terms, we have

  u⟨σ⟩        substitution,
  u,v         the dependent pairing of two terms,
  Pr₁, Pr₂    the two term-level projections 
  Lam u       the lambda abstraction (= currying) of a term u,
  App u v     the application of a term to another,
  q           the (second) context projection,
  |A|         the conversion of a type A into a term of type U,
  T_ u        various "syntactical transports" of a term u,
              replacing corresponding judgmental equalities.

\begin{code}

data Term where
  _⟨_⟩  : {i j k : Level} {Γ : Cxt i} {Δ : Cxt j} {A : Type k Γ} →
          Term Γ A → (σ : Subst Δ Γ) → Term Δ (A [ σ ])

  _,_   : {i j k : Level} {Γ : Cxt i} {A : Type j Γ} {B : Type k (Γ · A)} →
          (u : Term Γ A) → Term Γ (B ⌜ u ⌝) → Term Γ (Sigma A B)

  Pr₁   : {i j k : Level} {Γ : Cxt i} {A : Type j Γ} {B : Type k (Γ · A)} →
          Term Γ (Sigma A B) → Term Γ A

  Pr₂   : {i j k : Level} {Γ : Cxt i} {A : Type j Γ} {B : Type k (Γ · A)} →
          (w : Term Γ (Sigma A B)) → Term Γ (B ⌜ Pr₁ w ⌝)

  Lam   : {i j k : Level} {Γ : Cxt i} {A : Type j Γ} {B : Type k (Γ · A)} →
          Term (Γ · A) B → Term Γ (Pi A B)

  App   : {i j k : Level} {Γ : Cxt i} {A : Type j Γ} {B : Type k (Γ · A)} →
          Term Γ (Pi A B) → (u : Term Γ A) → Term Γ (B ⌜ u ⌝)

  q     : {i j : Level} {Γ : Cxt i} {A : Type j Γ} →
          Term (Γ · A) (A [ p ])

  ∣_∣    : {i j : Level} {Γ : Cxt i} →
          Type j Γ → Term Γ (U j)

-- Syntactic transports:

  T₀    : {i j k l : Level} {Γ : Cxt i} {Δ : Cxt j} {Ξ : Cxt k} {A : Type l Γ}
          {σ : Subst Δ Γ} {δ : Subst Ξ Δ} →
          Term Ξ (A [ σ ] [ δ ]) → Term Ξ (A [ σ ◦ δ ])

  T₁    : {i j : Level} {Γ : Cxt i} {A : Type j Γ} →
          Term Γ A → Term Γ (A [ I ])

  T₂    : {i j k l : Level} {Γ : Cxt i} {Δ : Cxt j} {A : Type k Γ} {B : Type l (Γ · A)}
          {u : Term Γ A} {σ : Subst Δ Γ} →
          Term Δ (B ⌜ u ⌝ [ σ ]) → Term Δ (B ⌈ σ ⌉ ⌜ u ⟨ σ ⟩ ⌝)

  T₃    : {i j k l : Level} {Γ : Cxt i} {Δ : Cxt j} {A : Type k Γ} {B : Type l (Γ · A)}
          {σ : Subst Δ Γ} →
          Term Δ ((Pi A B) [ σ ]) → Term Δ (Pi (A [ σ ]) (B ⌈ σ ⌉))

  T₄    : {i j k l : Level} {Γ : Cxt i} {Δ : Cxt j} {A : Type k Γ} {B : Type l (Γ · A)}
          {σ : Subst Δ Γ} →
          Term Δ ((Sigma A B) [ σ ]) → Term Δ (Sigma (A [ σ ]) (B ⌈ σ ⌉))

-- Backward versions:

  T⁰    : {i j k l : Level} {Γ : Cxt i} {Δ : Cxt j} {Ξ : Cxt k} {A : Type l Γ}
          {σ : Subst Δ Γ} {δ : Subst Ξ Δ} →
          Term Ξ (A [ σ ◦ δ ]) → Term Ξ (A [ σ ] [ δ ])

  T¹    : {i j : Level} {Γ : Cxt i} {A : Type j Γ} →
          Term Γ (A [ I ]) → Term Γ A

  T²    : {i j k l : Level} {Γ : Cxt i} {Δ : Cxt j} {A : Type k Γ} {B : Type l (Γ · A)}
          {u : Term Γ A} {σ : Subst Δ Γ} →
          Term Δ (B ⌈ σ ⌉ ⌜ u ⟨ σ ⟩ ⌝) → Term Δ (B ⌜ u ⌝ [ σ ])

  T³    : {i j k l : Level} {Γ : Cxt i} {Δ : Cxt j} {A : Type k Γ} {B : Type l (Γ · A)}
          {σ : Subst Δ Γ} →
          Term Δ (Pi (A [ σ ]) (B ⌈ σ ⌉)) → Term Δ ((Pi A B) [ σ ])

  T⁴    : {i j k l : Level} {Γ : Cxt i} {Δ : Cxt j} {A : Type k Γ} {B : Type l (Γ · A)}
          {σ : Subst Δ Γ} →
          Term Δ (Sigma (A [ σ ]) (B ⌈ σ ⌉)) → Term Δ ((Sigma A B) [ σ ])

\end{code}

Here is our definitions of the macros:

\begin{code}

B ⌜ u ⌝ = B [ ₍ I , T₁ u ₎ ]
u ⌞ v ⌟ = u ⟨ ₍ I , T₁ v ₎ ⟩
B ⌈ σ ⌉ = B [ ₍ σ ◦ p , T₀ q ₎ ]
u ⌊ σ ⌋ = u ⟨ ₍ σ ◦ p , T₀ q ₎ ⟩

\end{code}

Now the standard interpretation of type theory in type theory, defined
by (structural) mutual recursion, of course, with context,
substitution, type and term interpretation functions:

  A context is interpreted as a "set".
  A substitution is interpreted as a function from contexts to contexts.
  A type is interpreted as a function from contexts to sets.
  A term is interpreted as a dependent function from contexts to types.

\begin{code}

cxt⟦_⟧   : {i : Level}                              → Cxt i     → Set i
subst⟦_⟧ : {i j : Level} {Δ : Cxt i} {Γ : Cxt j}    → Subst Δ Γ → cxt⟦ Δ ⟧ → cxt⟦ Γ ⟧
type⟦_⟧  : {i j : Level} {Γ : Cxt i}                → Type j Γ  → cxt⟦ Γ ⟧ → Set j
term⟦_⟧  : {i j : Level} {Γ : Cxt i} {A : Type j Γ} → Term Γ A  → (γ : cxt⟦ Γ ⟧) → type⟦ A ⟧ γ

cxt⟦ ε ⟧           = []
cxt⟦ Γ · A ⟧       = Σ \(γ : cxt⟦ Γ ⟧) → type⟦ A ⟧ γ

type⟦ A [ σ ] ⟧    = λ γ → type⟦ A ⟧(subst⟦ σ ⟧ γ)
type⟦ Sigma A B ⟧  = λ γ → Σ \(u : type⟦ A ⟧ γ) → type⟦ B ⟧(γ , u)
type⟦ Pi A B ⟧     = λ γ → (u : type⟦ A ⟧ γ) → type⟦ B ⟧(γ , u)
type⟦ U i ⟧        = λ γ → Set i
type⟦ El u ⟧       = term⟦ u ⟧

subst⟦ I ⟧         = λ γ → γ
subst⟦ σ ◦ τ ⟧     = λ γ → subst⟦ σ ⟧(subst⟦ τ ⟧ γ)
subst⟦ p ⟧         = pr₁
subst⟦ ₍ σ , u ₎ ⟧ = λ γ → (subst⟦ σ ⟧ γ , term⟦ u ⟧ γ)

term⟦ u ⟨ σ ⟩ ⟧    = λ γ → term⟦ u ⟧ (subst⟦ σ ⟧ γ)
term⟦ q ⟧          = pr₂
term⟦ T₀ u ⟧       = term⟦ u ⟧
term⟦ T₁ t ⟧       = term⟦ t ⟧
term⟦ T₂ v ⟧       = term⟦ v ⟧
term⟦ T₃ u ⟧       = term⟦ u ⟧
term⟦ T₄ t ⟧       = term⟦ t ⟧
term⟦ u , v ⟧      = λ γ → (term⟦ u ⟧ γ , term⟦ v ⟧ γ)
term⟦ Pr₁ w ⟧      = λ γ → pr₁(term⟦ w ⟧ γ)
term⟦ Pr₂ w ⟧      = λ γ → pr₂(term⟦ w ⟧ γ)
term⟦ Lam u ⟧      = λ γ v → term⟦ u ⟧(γ , v)
term⟦ App u v ⟧    = λ γ → term⟦ u ⟧ γ (term⟦ v ⟧ γ)
term⟦ ∣ A ∣ ⟧       = type⟦ A ⟧
term⟦ T⁰ u ⟧       = term⟦ u ⟧
term⟦ T¹ t ⟧       = term⟦ t ⟧
term⟦ T² v ⟧       = term⟦ v ⟧
term⟦ T³ u ⟧       = term⟦ u ⟧
term⟦ T⁴ t ⟧       = term⟦ t ⟧

\end{code}

The funny order in the patterns in the definition of the
interpretation of terms comes from Agda's whim (if we reorder them
according to our taste, the file fails to typecheck).

All the required equations hold definitionally in the semantics.

The equations below labelled "eq" don't rely on the "transport" term
constructors T₀-T₄, but the ones labelled "Eq" do (either explicitly
or implicitly via the "macros" defined above).

\begin{code}

eq₀ : {i j : Level} {Δ : Cxt i} {Γ : Cxt j} {σ : Subst Δ Γ}

    → subst⟦ I ◦ σ ⟧ ≡ subst⟦ σ ◦ I ⟧
      -------------------------------
eq₀ = refl


eq₁ : {i j : Level} {Δ : Cxt i} {Γ : Cxt j} {σ : Subst Δ Γ}

    → subst⟦ σ ◦ I ⟧ ≡ subst⟦ σ ⟧
      ---------------------------
eq₁ = refl


eq₂ : {i₀ i₁ i₂ i₃ : Level} {Γ₀ : Cxt i₀} {Γ₁ : Cxt i₁} {Γ₂ : Cxt i₂} {Γ₃ : Cxt i₃}
      {ν : Subst Γ₀ Γ₁} {δ : Subst Γ₁ Γ₂} {σ : Subst Γ₂ Γ₃}

    → subst⟦ (σ ◦ δ) ◦ ν ⟧ ≡ subst⟦ σ ◦ (δ ◦ ν) ⟧
      -------------------------------------------
eq₂ = refl


eq₃ : {i j : Level} {Γ : Cxt i} {A : Type j Γ}

    → type⟦ A [ I ] ⟧ ≡ type⟦ A ⟧
      ---------------------------
eq₃ = refl


eq₄ : {i j k l : Level} {Γ : Cxt i} {Δ : Cxt j} {Ξ : Cxt k}
      {τ : Subst Ξ Δ} {σ : Subst Δ Γ} {A : Type l Γ}

    → type⟦ A [ σ ] [ τ ] ⟧ ≡ type⟦ A [ σ ◦ τ ] ⟧
      -------------------------------------------
eq₄ = refl


eq₅ :  {i j : Level} {Γ : Cxt i} {A : Type j Γ} {u : Term Γ A}

    → term⟦ u ⟨ I ⟩ ⟧ ≡ term⟦ u ⟧
      ---------------------------
eq₅ = refl


eq₆ : {i j k l : Level} {Γ : Cxt i} {Δ : Cxt j} {Ξ : Cxt k}
      {τ : Subst Ξ Δ} {σ : Subst Δ Γ} {A : Type l Γ} {u : Term Γ A}

    → term⟦ u ⟨ σ ⟩ ⟨ τ ⟩ ⟧ ≡ term⟦ u ⟨ σ ◦ τ ⟩ ⟧
      -------------------------------------------
eq₆ = refl


Eq₇ : {i j k l : Level} {Γ : Cxt i} {Δ : Cxt j} {Ξ : Cxt k} {A : Type l Γ}
      {σ : Subst Δ Γ} {u : Term Δ (A [ σ ])} {δ : Subst Ξ Δ}

    → subst⟦ ₍ σ , u ₎ ◦ δ ⟧ ≡ subst⟦ ₍ σ ◦ δ , T₀ (u ⟨ δ ⟩) ₎ ⟧
      ----------------------------------------------------------
Eq₇ = refl


eq₈ : {i j k : Level} {Γ : Cxt i} {Δ : Cxt j} {A : Type k Γ}
      {σ : Subst Δ Γ} {u : Term Δ (A [ σ ])}

    → subst⟦ p ◦ ₍ σ , u ₎ ⟧ ≡ subst⟦ σ ⟧
      -----------------------------------
eq₈ = refl


eq₉ : {i j k : Level} {Γ : Cxt i} {Δ : Cxt j} {A : Type k Γ}
      {σ : Subst Δ Γ} {u : Term Δ (A [ σ ])}

    → term⟦ q ⟨ ₍ σ , u ₎ ⟩ ⟧ ≡ term⟦ u ⟧
      -----------------------------------
eq₉ = refl


Eq₁₀ : {i j k l : Level} {Γ : Cxt i} {Δ : Cxt j} {A : Type k Γ} {B : Type l (Γ · A)} →
       {w : Term Γ (Pi A B)} {u : Term Γ A} {σ : Subst Δ Γ}

     → term⟦ (App w u) ⟨ σ ⟩ ⟧ ≡ term⟦ App (T₃ (w ⟨ σ ⟩)) (u ⟨ σ ⟩) ⟧
       --------------------------------------------------------------
Eq₁₀ = refl


Eq₁₁ : {i j k l : Level} {Γ : Cxt i} {Δ : Cxt j} {A : Type k Γ} {B : Type l (Γ · A)}
       {v : Term (Γ · A) B} {σ : Subst Δ Γ}

     → term⟦ (Lam v) ⟨ σ ⟩ ⟧ ≡ term⟦ Lam (v ⌊ σ ⌋) ⟧
       ---------------------------------------------
Eq₁₁ = refl


Eq₁₂ : {i j k : Level} {Γ : Cxt i} {A : Type j Γ} {B : Type k (Γ · A)}
       {w : Term Γ (Pi A B)}

     → term⟦ Lam (App (T₃ (w ⟨ p ⟩)) q) ⟧ ≡ term⟦ w ⟧
       ----------------------------------------------
Eq₁₂ = refl


eq₁₃ : {i j k : Level} {Γ : Cxt i} {A : Type j Γ} {B : Type k (Γ · A)}
       {u : Term (Γ · A) B} {v : Term Γ A}

     → term⟦ App (Lam u) v ⟧ ≡ term⟦ u ⌞ v ⌟ ⟧
       ---------------------------------------
eq₁₃ = refl


Eq₁₄ : {i j k l : Level} {Γ : Cxt i} {Δ : Cxt j} {A : Type k Γ} {B : Type l (Γ · A)}
       {σ : Subst Δ Γ}

     → type⟦ (Pi A B) [ σ ] ⟧ ≡ type⟦ Pi (A [ σ ]) (B ⌈ σ ⌉) ⟧
       -------------------------------------------------------
Eq₁₄ = refl


Eq₁₅ : {i j k l : Level} {Γ : Cxt i} {Δ : Cxt j} {A : Type k Γ} {B : Type l (Γ · A)}
       {σ : Subst Δ Γ}

     → type⟦ (Sigma A B) [ σ ] ⟧ ≡ type⟦ Sigma (A [ σ ]) (B ⌈ σ ⌉) ⟧
       -------------------------------------------------------------
Eq₁₅ = refl


Eq₁₆ : {i j k l : Level} {Γ : Cxt i} {Δ : Cxt j} {A : Type k Γ} {B : Type l (Γ · A)}
       {u : Term Γ A} {v : Term Γ (B ⌜ u ⌝)} {σ : Subst Δ Γ}

     → term⟦ (u , v) ⟨ σ ⟩ ⟧ ≡ term⟦ (u ⟨ σ ⟩ , T₂(v ⟨ σ ⟩)) ⟧
       -------------------------------------------------------
Eq₁₆ = refl


eq₁₇ : {i j k : Level} {Γ : Cxt i} {A : Type j Γ} {B : Type k (Γ · A)}
       {u : Term Γ A} {v : Term Γ (B ⌜ u ⌝)}

     → term⟦ Pr₁ (u , v) ⟧ ≡ term⟦ u ⟧
       --------------------------------
eq₁₇ = refl


eq₁₈ : {i j k : Level} {Γ : Cxt i} {A : Type j Γ} {B : Type k (Γ · A)}
       {u : Term Γ A} {v : Term Γ (B ⌜ u ⌝)}

     → term⟦ Pr₂ (u , v) ⟧ ≡ term⟦ v ⟧
       --------------------------------
eq₁₈ = refl


Eq₁₉ : {i j k l : Level} {Γ : Cxt i} {Δ : Cxt j} {A : Type k Γ} {B : Type l (Γ · A)}
       {t : Term Γ (Sigma A B)} {σ : Subst Δ Γ}

     → term⟦ (Pr₁ t) ⟨ σ ⟩ ⟧ ≡ term⟦ Pr₁ (T₄ (t ⟨ σ ⟩)) ⟧
       -------------------------------------------------
Eq₁₉ = refl


Eq₂₀ : {i j k l : Level} {Γ : Cxt i} {Δ : Cxt j} {A : Type k Γ} {B : Type l (Γ · A)}
       {t : Term Γ (Sigma A B)} {σ : Subst Δ Γ}

     → term⟦ (Pr₂ t) ⟨ σ ⟩ ⟧ ≡ term⟦ Pr₂ (T₄ (t ⟨ σ ⟩)) ⟧
       --------------------------------------------------
Eq₂₀ = refl


eq₂₁ : {i j : Level} {Γ : Cxt i} {A : Type j Γ} →
     let p' = p {i} {j} {Γ} {A}
         q' = q {i} {j} {Γ} {A}
         I' = I {j ⊔ i} {Γ · A}

     in subst⟦ ₍ p' , q' ₎ ⟧ ≡ subst⟦ I' ⟧
       -----------------------------------
eq₂₁ = refl


eq₂₂ : {i j : Level} {Γ : Cxt i} {A : Type j Γ}

     → type⟦ El ∣ A ∣ ⟧ ≡ type⟦ A ⟧
       --------------------------
eq₂₂ = refl


eq₂₃ : {i j : Level} {Γ : Cxt i} {u : Term Γ (U j)}

     → term⟦ ∣ El u ∣ ⟧ ≡ term⟦ u ⟧
       --------------------------
eq₂₃ = refl

\end{code}

To do: 

  Now, once the terms, types, substitutions and contexts have been
  defined and interpreted, define congruences on them, and prove that
  the interpretation transforms congruence into *definitional*
  equality, as in the above equations.  We believe we can see that
  this is the case.

  Next, define the presheaf interpretation. (We believe that all the
  equations that currently hold definitionally will only hold
  propositionally.)