• General
• What is the logic of Coq?
• Is Coq's logic intuitionistic or classical?
• How does the logic of Coq compare to the one of Agda, Isabelle, Lean, Mizar, ...
• Can I define non-terminating programs in Coq?
• How is equational reasoning working in Coq?
• Axioms
• What axioms can be safely added to Coq?
• What is the standard model of Coq?
• What is Streicher's axiom K?
• What is proof-irrelevance?
• What about functional extensionality?
• Is Prop impredicative?
• Is Set impredicative?
• Is Type impredicative?
• I have two proofs of the same proposition. Can I prove they are equal?
• I have two proofs of an equality statement. Can I prove they are equal?
• Can I prove that the second components of equal dependent pairs are equal?
• Impredicativity
• Do False, eq, and Acc have a special status?
• Is Coq’s logic conservative over Coquand’s Calculus of Constructions?
• References