Primitives: elements, sets.
Functions are a derived construction.
Primitives: functions, types.
Elements are a derived construction.
Sologan:
types are like sets that remember their definition.
sets
props
(proof) pf of (prop) P becomes pf : P
rules of inference
proof verification
propositional calculus: constructions on proposition types
This well-formed tree is the proof term
With have enough basic foundation to finally have a look at
![]() |
![]() |
Formalize fundamental theorems in Differential Geometry in Lean:
Columns in Marp: https://github.com/orgs/marp-team/discussions/192