Theorem hSet_univalence (X Y : hSet) : (X = Y) ≃ (X ≃ Y). Proof. Set Printing Coercions. intros. set (f := hSet_univalence_map X Y). exists f. set (g := @eqweqmap (pr1 X) (pr1 Y)). set (h := λ e : X = Y, maponpaths pr1hSet e). assert (comp : f = g ∘ h). { apply funextfun; intro e. induction e. apply idpath. } induction (!comp). apply twooutof3c. - apply isweqonpathsincl. apply isinclpr1. exact isapropisaset. - apply univalenceAxiom. Unset Printing Coercions. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.