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

---
 ex/HoTT book/Ch1.thy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ex/HoTT book/Ch1.thy')

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)"
-- 
cgit v1.2.3

