(A : Ordinal) : Ordinal. Proof. set (carrier := (A + Unit)%type). set (relation (x y : carrier) := match x, y with | inl x, inl y => x < y | inl x, inr _ => Unit | inr _, inl y => Empty | inr _, inr _ => Empty end). exists carrier relation. constructor. - exact _. - intros [x | ?] [y | ?]; cbn; exact _. - intros [x | []] [y | []] H. + f_ap. apply extensionality. intros z. exact (H (inl z)). + enough (H0 : relation (inl x) (inl x)). { cbn in H0. destruct (irreflexivity _ _ H0). } apply H. cbn. exact tt. + enough (H0 : relation (inl y) (inl y)). { cbn in H0. destruct (irreflexivity _ _ H0). } apply H. cbn. exact tt. + reflexivity. - assert (H : forall a, Accessible relation (inl a)). { intros a. induction (well_foundedness a) as [a _ IH]. constructor; intros [b | []]; cbn; intros H. + apply IH. exact H. + destruct H. } intros [x | []]. + apply H. + constructor; intros [b | []]; cbn; intros H0. * apply H. * destruct H0. - intros [x | []] [y | []] [z | []]; cbn; auto. intros _ []. Defined.
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.