aboutsummaryrefslogtreecommitdiff
path: root/ex
diff options
context:
space:
mode:
Diffstat (limited to 'ex')
-rw-r--r--ex/HoTT book/Ch1.thy2
-rw-r--r--ex/Synthesis.thy2
2 files changed, 2 insertions, 2 deletions
diff --git a/ex/HoTT book/Ch1.thy b/ex/HoTT book/Ch1.thy
index 65de875..cc0adf5 100644
--- a/ex/HoTT book/Ch1.thy
+++ b/ex/HoTT book/Ch1.thy
@@ -13,7 +13,7 @@ chapter \<open>HoTT Book, Chapter 1\<close>
section \<open>1.6 Dependent pair types (\<Sigma>-types)\<close>
-text "Prove that the only inhabitants of the \<Sigma>-type are those given by the pair constructor."
+text "Propositional uniqueness principle:"
schematic_goal
assumes "(\<Sum>x:A. B(x)): U(i)" and "p: \<Sum>x:A. B(x)"
diff --git a/ex/Synthesis.thy b/ex/Synthesis.thy
index cd5c4e1..e5a8ecf 100644
--- a/ex/Synthesis.thy
+++ b/ex/Synthesis.thy
@@ -76,4 +76,4 @@ theorem
by (simple lems: pred_welltyped pred_type pred_props)
-end \ No newline at end of file
+end