A type theory that can serve as a programming language and as constructive foundations for math proofs.
Setup
Every definition has two parts:
- Introduction: How the type is created
- Elimination: How the type is used and creates different types
A type theory that can serve as a programming language and as constructive foundations for math proofs.
Every definition has two parts: