de brujin principle: the program should have a small, trusted kernel responsible for checking theorems
kernel -> rules of type theory
dtt: · impredicative uniferse prop def proof irrrelevance no univ cumul indexed · inductive types: e.g. ℕ in the DTT notaation: K ::= 0 | (c:e) + K e ::= …|μx : eK | c_{μx:e.K} | rec_{μx:e.K} and in particular: ℕ := μT : U₁ . (zero : T) + (succ : T → T) such a def is only admissible if positive (no T on the left side of an arrow) something goes against cantor’s theorem?
lean: treat all proofs of a prop as the same zfc: axioms of set theory that all mathematicians % french agree on idea: treat types as sets and elements as elements of the set (= obv model of dtt in zfc)
grothendieck universes?
lean is proven consistent if zfc with ω inaccessible is consistent
definitional inversion theorem
understand proofs?