From 6b9cf8c6752d2f928dfd4e7b0d3584e1c01002b3 Mon Sep 17 00:00:00 2001 From: Carlo Angiuli Date: Thu, 1 Aug 2024 11:28:43 -0500 Subject: [PATCH] add one exercise/solution for lecture 5 --- .../set_level_mathematics_exercises.v | 6 ++++++ .../set_level_mathematics_solutions.v | 8 ++++++++ 2 files changed, 14 insertions(+) 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.