The Type Theory of Lean [Thesis]

Introduction
	Type theory in programming languages
	Set theoretic models of type theory
The axioms
	Typing
	Definitional equality
	Reduction
	let binders ( reduction)
	Definitions ( reduction)
	Inductive types
		Inductive specifications
		Large elimination
		The recursor
		The computation rule ( reduction)
	Non-primitive axioms
		Quotient types
		Propositional extensionality
		Axiom of choice
	Differences from Coq
Properties of the type system
	Undecidability of definitional equality
		Algorithmic equality is not transitive
		Failure of subject reduction
	Regularity
Unique typing
	The  reduction
	The Church-Rosser theorem
Reduction of inductive types to W-types
	The menagerie
	Translating type families
	Translating subsingleton eliminators
	The remainder
Soundness
	Proof splitting
	Modeling Lean in ZFC
		Definition of W-types in ZFC
		Definition of acc in ZFC
	Soundness
	Type injectivity