Type Theory and its Meaning Explanations

TL;DR

This paper explores the semantics of intuitionistic type theory, emphasizing the shift from proof-centric to verification-centric understanding through meaning explanations and contrasting different approaches to type theories.

Contribution

It clarifies how meaning explanations underpin intuitionistic type theory and distinguishes between semantics-based and proof-theoretic interpretations.

Findings

Meaning explanations redefine core notions from proof to verification.

Type theories can be viewed as enrichments of logical theories with additional judgements.

Contrast between semantics-based and proof-theoretic approaches to type theory.

Abstract

At the heart of intuitionistic type theory lies an intuitive semantics called the "meaning explanations"; crucially, when meaning explanations are taken as definitive for type theory, the core notion is no longer "proof" but "verification". We'll explore how type theories of this sort arise naturally as enrichments of logical theories with further judgements, and contrast this with modern proof-theoretic type theories which interpret the judgements and proofs of logics, not their propositions and verifications.