A (basic) understanding of extensional type theory

This is first and foremost a pre-meeting log for chatting with Jon Sterling. Questions for the meeting are marked Q^Jon:like this.

Chapter 2 of Principles of Dependent Type Theory (from here on known as The Book) concerns itself with defining the rules of type theory. It begins with the classical formulation of STLC, but quickly moves on to define the concept of the "substitution calculus".

The substitution calculus is a category where objects are contexts, and morphisms are (backwards) parallel substitutions. The empty context is terminal. Thinking back to formalizing different calculi I would also expect that parallel substitution is the right notion here. On this we have a set (presheaf) of types Ty(Γ), along with another set of terms Tm(Γ, A) where A ∈ Ty(Γ). There is a natural way to apply substitutions on types and terms. Given a context Γ and a type Ty(Γ), we can construct a context Γ.A. Terms Tm(Γ, A) induce a map from Γ ⟶ Γ.A. We have a special substitution Γ.A ⊢ p : Γ, this is weakening. We also have a special term Γ ⊢ A type => Γ.A ⊢ q : A[p], the reason there is a p on the A is so the precondition holds. For a reason I am slightly confused about they also introduce the notation γ* ≔ λ ξ ↦ ξ ∘ γ which they "the restriction map". Q^Jon:Would be great to chat about what this is / where it comes from.

In the descriptions of type theory I was used to, I would expect the next step would be, for each connective:

• Formation rules: Σ (c : X), Y c
• Introduction rules: ⟨u, v⟩
• Elimination rules: let ⟨u, v⟩ := x in body
• β rules: let ⟨u, v⟩ := ⟨a, b⟩ in body ⇝ body[id.u ↦ a.v ↦ b]
• η rules: let ⟨u, v⟩ := x in ⟨u, v⟩ = x

Instead The Book goes on to talk about how each of these can be derived from a (natural) isomorphism. This was quite surprising as to me, connectives in a theory correspond to different universal properties of the source category. For example the CCC structure induces exactly the 3 connectives one would expect in STLC. Through conversations with Beatrice, she told me a fact that natural isomorphisms on presheafs correspond to universal properties in the source category. Q^Jon:Would be nice to chat about this a bit to make sure I understand it. Nonetheless the key idea can bee sen in Slogan 2.5.5:

1. a natural isomorphism relating Tm(Γ, Υ) to judgmentally-determined structure, or
2. a collection of natural term constructors for Υ which, for all Γ.Υ ⊢ 𝐴 type, determine a natural isomorphism relating Tm(Γ.Υ, 𝐴) to judgmentally-determined structure.

I find the exact constructions quite involved and will try to work with them a bit to actually get a feel for how they operate. Q^Jon:If you have some more resources on this construction I would happily read them.

• Q^Jon:Do you have any resources on conservativity?
• Q^Jon:Do you have any writings on how these natural transformations work with observational equality?
• Q^Jon:What will be the exact mechanism to cross the boundary from MLTT and OTT++
• Q^Jon:What are some next steps after working through The Book?