proposition: Lemma path_simulation `{Funext} {A B : Ordinal} (f : A -> B) {is_simulation_f : IsSimulation f} (g : A -> B) {is_simulation_g : IsSimulation g} : f = g.
proof: 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.
imports: HoTT(TruncType ExcludedMiddle Modalities.ReflectiveSubuniverse abstract_algebra) HoTT(PropResizing.PropResizing) HoTT(Colimits.Quotient) HoTT(HSet)