From 41f13f91d023e497d9b35e7a958a961aa0c7a5e5 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sat, 18 Aug 2018 14:34:08 +0200
Subject: Misc formatting

---
 ProdProps.thy        | 1 -
 ex/HoTT book/Ch1.thy | 2 +-
 ex/Synthesis.thy     | 2 +-
 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
-- 
cgit v1.2.3