• Proof irrelevance
• Axiom K / Uniqueness of Identity Proofs
• Functional extensionality
• Propositional extensionality
• Excluded middle (classical logic)
• Strong excluded middle
• Axiom of choice
• Indefinite description / Hilbert's epsilon operator
• Summary