proposition: Theorem hSet_rect (X Y : hSet) (P : X ≃ Y -> UU) : (∏ e : X=Y, P (hSet_univalence _ _ e)) -> ∏ f, P f.
proof: 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.
imports: UniMath.Foundations.Propositions UniMath.Foundations.UnivalenceAxiom