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