`{Univalence} (A B : Ordinal) : Isomorphism A B <~> A = B. Proof. unfold Isomorphism. rapply symmetric_equiv. transitivity (equiv_Ordinal_to_sig A = equiv_Ordinal_to_sig B). { apply equiv_ap'. } transitivity ((equiv_Ordinal_to_sig A).1 = (equiv_Ordinal_to_sig B).1). { exists pr1_path. exact (isequiv_pr1_path_hprop _ _). } transitivity (exist Relation A (<) = exist Relation B (<)). { reflexivity. } transitivity { p : A = B :> Type & p # (<) = (<) }. { symmetry. exact (equiv_path_sigma Relation (exist Relation A (<)) (exist Relation B (<))). } srapply equiv_functor_sigma'. - exact (equiv_equiv_path A B). - cbn. intros p. nrapply equiv_iff_hprop. + apply (istrunc_equiv_istrunc (forall b b' : B, (p # (<)) b b' = (b < b'))). { transitivity (forall b : B, (p # lt) b = lt b). { apply equiv_functor_forall_id; intros b. apply equiv_path_arrow. } apply equiv_path_arrow. } exact _. + exact _. + intros <- a a'. rewrite transport_arrow. rewrite transport_arrow_toconst. repeat rewrite transport_Vp. reflexivity. + intros H0. by_extensionality b. by_extensionality b'. rewrite transport_arrow. rewrite transport_arrow_toconst. apply path_iff_ishprop_uncurried. specialize (H0 (transport idmap p^ b) (transport idmap p^ b')). repeat rewrite transport_pV in H0. exact H0. 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.