Notes on Propositional Equality

1 · Jonathan Chan · May 25, 2021, midnight
Table of Contents Inductively-Defined Equality The J Eliminator Uniqueness Rule for J The K Eliminator UIP from K Heterogeneous Equality UIP from J* J and K from J* Substitution and Contractibility of Singletons J and K by Substitution Congruence and Coercion Congruence with Dependent Functions Regularity Mid-Summary Extensional Equality Function Extensionality Propositional Truncation/Squash Types Quotient Types Effectiveness Squashes from Quotients Higher Inductive Types Th...