Sets in Coq, Coq in Sets

Downloadable resources:

• A paper describing the formalization (published in the Journal of Formalized Reasoning)
• Download the proofs (.tgz)

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
• Classical Ordinal Numbers
• Fixpoint Theorem
• Grothendieck Universes
• Lambda terms
• Cardinal Numbers
• Semantics of CC in ZF
• Semantics of CCω in Tarski-Grothendieck Set Theory
• Inductive Types Nat and Ord
• Type Theoretical Axiom of Choice
• 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

Calculus of Constructions

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

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)
• Pure Lambda Terms
• Reducibility Candidates and Operations
• Generic Interface of Saturated Sets
• Soundness of Abstract Strong Normalization Models of CC
• Another Proof of Strong Normalization for the Calculus of Constructions

General Purpose Libraries

• Useful definitions
• Maps