  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.
