§ 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: