proposition: Lemma path_initial_segment_simulation `{Univalence} `{PropResizing} {A : Type} {R : Lt A} `{IsOrdinal A R} {B : Type} {Q : Lt B} `{IsOrdinal B Q} (f : A -> B) {is_simulation : IsSimulation f} (a : A) : ↓(f a) = ↓a.
proof: Proof. apply equiv_path_Ordinal. apply (equiv_initial_segment_simulation f). Qed.
imports: HoTT(TruncType ExcludedMiddle Modalities.ReflectiveSubuniverse abstract_algebra) HoTT(PropResizing.PropResizing) HoTT(Colimits.Quotient) HoTT(HSet)