 This Axiom can be seen as a strong form of the extensionality principle. It indeed generalizes the Axiom of propositional extensionality mentioned by Church 1940, which states that two logically equivalent propositions are equal. Surprisingly, it also implies the Axiom of function extensionality, Axiom 10 in Church 1940, which states that two pointwise equal functions are equal (Voevodsky 2015). It also directly implies that two isomorphic sets are equal, that two categorically equivalent groupoids are equal, and so one. 