aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--ProdProps.thy1
-rw-r--r--ex/HoTT book/Ch1.thy2
-rw-r--r--ex/Synthesis.thy2
3 files changed, 2 insertions, 3 deletions
diff --git a/ProdProps.thy b/ProdProps.thy
index 7071b39..adadb29 100644
--- a/ProdProps.thy
+++ b/ProdProps.thy
@@ -21,7 +21,6 @@ text "
lemma compose_assoc:
assumes "A: U(i)" and "f: A \<rightarrow> B" "g: B \<rightarrow> C" "h: \<Prod>x:C. D(x)"
shows "(h \<circ> g) \<circ> f \<equiv> h \<circ> (g \<circ> f)"
-
proof (subst (0 1 2 3) compose_def)
show "\<^bold>\<lambda>x. (\<^bold>\<lambda>y. h`(g`y))`(f`x) \<equiv> \<^bold>\<lambda>x. h`((\<^bold>\<lambda>y. g`(f`y))`x)"
proof (subst Prod_eq)
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