§ Mostowski Collapse

§ Image of collapse is transitive

§ Image of collapse is order embedding if RR is extensional

§ Forward: v1<v2    π(v1)π(v2)v_1 < v_2 \implies \pi(v_1) \in \pi(v_2):

§ Backward: π(v1)π(v2)    v1<v2\pi(v_1) \in \pi(v_2) \implies v_1 < v_2:

§ Collapse is injective: