Propositional equality

Redirect to:

• Type theory#Equality types