`{Funext} {A B : Ordinal} (f : A -> B) {is_simulation_f : IsSimulation f} (g : A -> B) {is_simulation_g : IsSimulation g} : f = g. Proof. apply path_forall; intros a. induction (well_foundedness a) as [a _ IH]. apply (extensionality (f a) (g a)). intros b. split. - intros b_fa. destruct (simulation_is_minimal f b_fa) as (a' & a'_a & <-). rewrite (IH _ a'_a). apply (simulation_is_hom g). exact a'_a. - intros b_ga. destruct (simulation_is_minimal g b_ga) as (a' & a'_a & <-). rewrite <- (IH _ a'_a). apply (simulation_is_hom f). exact a'_a. 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.