diff --git a/2024-07-Minneapolis/5_Set-level-mathematics/set_level_mathematics_exercises.v b/2024-07-Minneapolis/5_Set-level-mathematics/set_level_mathematics_exercises.v
index 51730b3..6bb77e5 100644
--- a/2024-07-Minneapolis/5_Set-level-mathematics/set_level_mathematics_exercises.v
+++ b/2024-07-Minneapolis/5_Set-level-mathematics/set_level_mathematics_exercises.v
@@ -213,6 +213,12 @@ Admitted.
 (* Once the goals are solved, replace "Admitted" by "Defined" *)
 (* Defined. *)
 
+Definition transportf_ptdset :
+  ∏ (P : ptdset → UU) (X Y : ptdset), ptdset_iso X Y → P X → P Y.
+Proof.
+  admit.
+Admitted.
+
 
 End Pointed.
 
diff --git a/2024-07-Minneapolis/5_Set-level-mathematics/set_level_mathematics_solutions.v b/2024-07-Minneapolis/5_Set-level-mathematics/set_level_mathematics_solutions.v
index 475079f..7b76166 100644
--- a/2024-07-Minneapolis/5_Set-level-mathematics/set_level_mathematics_solutions.v
+++ b/2024-07-Minneapolis/5_Set-level-mathematics/set_level_mathematics_solutions.v
@@ -235,6 +235,14 @@ Proof.
   - apply ptdset_iso_weq.
 Defined.
 
+Definition transportf_ptdset :
+  ∏ (P : ptdset → UU) (X Y : ptdset), ptdset_iso X Y → P X → P Y.
+Proof.
+  intros P X Y f.
+  apply sip_for_ptdset in f.
+  exact (transportf P f).
+Defined.
+
 
 End Pointed.