Intuitionistic Set Theory and Type Theories with Inductive Families

Intuitionistic Zermelo-Fraenkel

• Signatures of IZF
• Introduction/Elimination Rules of IZF Axioms
• Relationnal Replacement Axiom
• Ordered pairs
• Relations and Functions
• Disjoint Sum
• Natural Numbers
• Ordinal Numbers
• Fixpoint Theorem
• Grothendieck Universes
• Lambda terms
• Isomorphisms
• Cardinal Numbers

• Semantics of CC in ZF
• Semantics of CCω in Tarski-Grothendieck Set Theory
• Inductive Type Nat
• Inductive Type W
• Inductive families (dependent W-types)
• Non-uniform parameters
• Nested inductive definitions

• Type Theoretical Axiom of Choice
• Model of IZF and ZF in Coq
• Skolemization of IZF (with support for classical versions)
• Model of IZF in Coq
• Building a Grothendieck Universe in Coq
• Skolemization of IZF

Hereditarily Finite Set Theory

• Hereditarily Finite Sets
• HF Relations
• Semantics of CC in HF

Syntax: Calculus of Constructions

• Terms
• Conversion
• Environments
• Typing Rules
• Typing Rules (judgemental equality + Adams' proof)

Syntax: Calculus of Constructions with Universes

• Terms
• Conversion
• Environments
• Typing Rules
• Typing Rules (judgemental equality)

Models of the Calculus of Constructions (pure and with universes)

• Abstract Models of CC and CCω
• Soundness of Abstract Models of CC
• Mapping CC Syntax to the Abstract Model of CC
• Instantiation of the Abstract Model of CC in HF
• Instantiation of the Abstract Model of CC in IZF
• Soundness of Abstract Models of CCω
• Model of CC with Natural Numbers (with type-based termination for fixpoints)

Strong Normalization models

• Pure Lambda Terms
• Reducibility Candidates and Operations
• Generic Interface of Saturated Sets

• Pseudo-syntax for strong normalization models
• Soundness of Abstract Strong Normalization Models of CC
• Another Proof of Strong Normalization for the Calculus of Constructions

• Soundness of Abstract Strong Normalization Models of CC (strong elimination)
• Yet another Proof of Strong Normalization for the Calculus of Constructions (compatible with strong elimination
• Reducibility theory of natural numbers
• Proof of Strong Normalization for the Calculus of Constructions extended with natural numbers (recursor)
• Proof of Strong Normalization for the Calculus of Constructions extended with natural numbers (type-based termination)

General Purpose Libraries