• Home
• About Coq
• Get Coq
• Documentation
• Community

Library IZF.IZF_union

Library IZF.IZF_select

Library IZF.IZF_power

Library IZF.IZF_pair

Library IZF.IZF_omega

• Zero
• The successor function
• The set of von Neuman numerals
  • The axiom of infinity

Library IZF.IZF_nat

• The type of Church numerals in Typ1
  • Definition of natural numbers
  • The predecessor function
• Deriving Peano's axioms
  • First axiom of Peano
  • Second axiom of Peano
  • Third axiom of Peano
  • Fourth axiom of Peano
  • Fifth axiom of Peano
• Ordering
  • Strict ordering

Library IZF.IZF_logic

• Universes
• Logical connectives
  • Truth and falsity
  • Conjunction
  • Disjunction
  • Logical equivalence
• Existential quantifiers and Leibniz equality
  • Existential quantification in a given small type
  • Existential quantification over all small types
  • Existential quantification over all pointed graphs
  • Leibniz equality
• Some data structures
  • Option type
  • Extended sum type

Library IZF.IZF_coll

• The intuitionistic Hilbert epsilon operator
• An implementation of a super-powerset
  • Building the carrier of the super-powerset
  • Building the edge relation of the super-powerset
• Compatible relations and the collection scheme
  • Binary relations
  • The collection scheme

Library IZF.IZF_base

• Equality as bisimilarity
• Membership as shifted bisimilarity
• Inclusion and extensionality
• Delocations

• webmaster
• xhtml valid
• CSS valid