`{PropResizing} `{Univalence} (O : Ordinal) (a : O) : Isomorphism O ↓a -> Empty. Proof. intros p % equiv_path_Ordinal. enough (HO : O < O) by apply (irreflexive_ordinal_relation _ _ _ _ HO). exists a. apply p. Qed.
From HoTT Require Import TruncType ExcludedMiddle Modalities.ReflectiveSubuniverse abstract_algebra. From HoTT Require Import Universes.Smallness. From HoTT Require Import Colimits.Quotient. From HoTT Require Import HSet.