From a1afde729f1d9b2f930696b117cfaec827eaa178 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Wed, 12 Sep 2018 06:33:55 +0200
Subject: Some final touchups before release 0.1 for the MS thesis

---
 Univalence.thy | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'Univalence.thy')

diff --git a/Univalence.thy b/Univalence.thy
index 80325f3..8599ba7 100644
--- a/Univalence.thy
+++ b/Univalence.thy
@@ -15,6 +15,8 @@ begin
 
 section \<open>Homotopy and equivalence\<close>
 
+text "We define polymorphic constants implementing the definitions of homotopy and equivalence."
+
 axiomatization homotopic :: "[Term, Term] \<Rightarrow> Term"  (infix "~" 100) where
   homotopic_def: "\<lbrakk>
     f: \<Prod>x:A. B x;
@@ -166,7 +168,7 @@ proof
 qed
 
 
-text "The univalence axiom:"
+text "The univalence axiom."
 
 axiomatization univalence :: Term where
   ua: "univalence: isequiv idtoeqv"
-- 
cgit v1.2.3