Intuitionistic Set Theory and Type Theories with Inductive Families
Download proofs (.tgz)
Intuitionistic Zermelo-Fraenkel
General libraries:
Type theoretical constructions:
Modeling set theory in type theory:
Hereditarily Finite Set Theory
Syntax: Calculus of Constructions
Syntax: Calculus of Constructions with Universes
Models of the Calculus of Constructions (pure and with universes)
Strong Normalization models
Theory of Reducibility candidates and Saturated Sets:
Simple strong elimination models (weak elimination only):
Supporting strong elimination:
General Purpose Libraries
Useful definitions
Maps
Table of contents of Coq objects
Back to upper level