Theorem hSet_rect (X Y : hSet) (P : X ≃ Y -> UU) : (∏ e : X=Y, P (hSet_univalence _ _ e)) -> ∏ f, P f. Proof. intros ih ?. Set Printing Coercions. set (p := ih (invmap (hSet_univalence _ _) f)). set (h := homotweqinvweq (hSet_univalence _ _) f). exact (transportf P h p). Unset Printing Coercions. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.