The metatheory of ETT and how terms form a presheaf

From chapter 2 we are introduced to ETT. ETT is a dependent type theory with a type of equalities induced by the natural isomorphism (ι : (Γ : Cx) → (A : Ty Γ) → (a b : Tm Γ A) → Tm Γ (Eq Γ (A, a, b)) ≅ { ⋆ | a = b } ) where Eq : (Γ : Cx) → ((A : Ty Γ) × Tm Γ A × Tm Γ A) → Ty Γ. A consequence of this rule is that judgemental and propositional equality coincide. This has some quite dire consequences for type-checking as we will come back to.

This chapter is structured in the following way:

• Type checking and elaboration
• Models of ETT and the Set model
• Undecidability of equality

First the Book begins by introducing a syntax (preterms) for dependent type theory. It then defines elaboration as the process of moving preterms to terms. Another way this can be viewed as type checking a preterm, to produce a term of a given type.

From there they also detail bidirectional elaboration as a system where both inference and checking are allowed. For this they add just one more rule: chk e τ to ensure a term e has type τ. This seems overly verbose as the type τ might be quite involved to write, thinking back to how Lean works, the type τ could maybe be a "pretype" that has holes in it. Q^Jon:Is there a principled way to follow this notion? Could chk "compute" on the pretype in some way?.

Further there is a quick aside on how definitions should work. The tool mentioned for this was a type Sing(A, a), where the A is the type of the definition and a is the body.

The next key section mentions models of ETT. A model of type theory is decomposed into a few parts parts.

• A category 𝓜 of contexts,
• the context structure 1 and - • = for context extensions along the,
• the presheaf Ty-𝓜 : PSh(𝓜) and Tm-𝓜 : PSh(∫ Ty-𝓜),
• implementations of each of the natural isomorphisms ι and ρ.

From here it is stated that the syntax of ETT quotiented by definitional equality (or, "the syntactic category" of ETT) is the initial object in the category of ETT models. This is then used to prove the consistency of the type theory, by considering a model 𝓜 for which Tm-𝓜(1, Void) is empty, we can see that a morphism m : Syn ⟶ 𝓜 would yield an empty set if Tm(1, Void) was inhabited. This then relies on the set model of the type theory.

Given ZF+(𝓤 (ω + 1)), ZF plus a hierarchy of Grothendieck, we can construct a model of ETT. Here we select 𝓤ω to be our contexts, and our types are given by Ty-Set(Γ) := Γ → 𝓤ω. The reason we pick the large universe as our contexts and types comes from the fact that we want to fit all smaller universes in it. One could imagine an extention ETT+ω, in this case we would need ZF+(𝓤 (ω + 2)).

A consequence of propositional equality coinciding with definitional equality, is that to type check Eq(ℕ → Bool, a, b), would require finding a proof of a and b being equal, this is exactly an example of a semi decidable problem.

It is not directly obvious to what extent terms form a presheaf. One can think of terms as some data that behaves nicely under substitution, and a map nominating their types. The direct structure for this is PSh(𝓒)/Ty. Though there turns out to be a structure whos presheafs encode this notion, known as the Grothendieck construction on Ty written ∫𝓒 Ty.

This structure then satisfies the equation PSh(C) / Ty ≅ PSh(∫𝓒 Ty). I will try to solve this by the meeting: