add one exercise/solution for lecture 5

UniMath · Aug 1, 2024 · 6b9cf8c · 6b9cf8c
1 parent 1c7c748
commit 6b9cf8c
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 0 deletions.
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
@@ -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
@@ -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.