• What standard axioms are inconsistent with impredicative Set?
• Why does injection not work on impredicative Set?
• What is a “large inductive definition”?
• Is Coq’s logic conservative over Coquand’s Calculus of Constructions?