proposition: Theorem UU_rect (X Y : UU) (P : X ≃ Y -> UU) : (∏ e : X=Y, P (univalence _ _ e)) -> ∏ f, P f.
proof: Proof. intros ih ?. set (p := ih (invmap (univalence _ _) f)). set (h := homotweqinvweq (univalence _ _) f). exact (transportf P h p). Defined.
imports: UniMath.Foundations.PartB