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

---
 Coprod.thy     | 2 +-
 EqualProps.thy | 4 ++--
 ProdProps.thy  | 2 +-
 Sum.thy        | 2 +-
 Unit.thy       | 2 +-
 Univalence.thy | 4 +++-
 6 files changed, 9 insertions(+), 7 deletions(-)

diff --git a/Coprod.thy b/Coprod.thy
index b87958a..1ff7361 100644
--- a/Coprod.thy
+++ b/Coprod.thy
@@ -28,7 +28,7 @@ and
     \<And>x. x: A \<Longrightarrow> c x: C (inl x);
     \<And>y. y: B \<Longrightarrow> d y: C (inr y);
     u: A + B
-    \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d u : C u"
+    \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d u: C u"
 and
   Coprod_comp_inl: "\<lbrakk>
     C: A + B \<longrightarrow> U i;
diff --git a/EqualProps.thy b/EqualProps.thy
index 4cfe280..5db8487 100644
--- a/EqualProps.thy
+++ b/EqualProps.thy
@@ -278,6 +278,8 @@ section \<open>Transport\<close>
 definition transport :: "Term \<Rightarrow> Term" where
   "transport p \<equiv> ind\<^sub>= (\<lambda>x. (\<^bold>\<lambda>x. x)) p"
 
+text "Note that \<open>transport\<close> is a polymorphic function in our formulation."
+
 lemma transport_type:
   assumes
     "A: U i" "P: A \<longrightarrow> U i"
@@ -292,7 +294,5 @@ lemma transport_comp:
   shows "transport (refl x) \<equiv> id"
 unfolding transport_def by (derive lems: assms)
 
-text "Note that in our formulation, \<open>transport\<close> is a polymorphic function!"
-
 
 end
diff --git a/ProdProps.thy b/ProdProps.thy
index 47e386b..a68f79b 100644
--- a/ProdProps.thy
+++ b/ProdProps.thy
@@ -14,7 +14,7 @@ begin
 section \<open>Composition\<close>
 
 text "
-  The proof of associativity needs some guidance; it involves telling Isabelle to use the correct rule for \<Pi>-type definitional equality, and the correct substitutions in the subgoals thereafter.
+  The proof of associativity needs some guidance; it involves telling Isabelle to use the correct rule for \<Prod>-type definitional equality, and the correct substitutions in the subgoals thereafter.
 "
 
 lemma compose_assoc:
diff --git a/Sum.thy b/Sum.thy
index 6de20fd..aac81f7 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -47,7 +47,7 @@ and
     a: A;
     b: B a;
     \<And>x y. \<lbrakk>x: A; y: B(x)\<rbrakk> \<Longrightarrow> f x y: C <x,y>;
-    B: A \<longrightarrow> U(i);
+    B: A \<longrightarrow> U i;
     C: \<Sum>x:A. B x \<longrightarrow> U i
     \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum> f <a,b> \<equiv> f a b"
 
diff --git a/Unit.thy b/Unit.thy
index 9b86739..6760f27 100644
--- a/Unit.thy
+++ b/Unit.thy
@@ -16,7 +16,7 @@ axiomatization
   pt :: Term    ("\<star>") and
   indUnit :: "[Term, Term] \<Rightarrow> Term"  ("(1ind\<^sub>\<one>)")
 where
-  Unit_form: "\<one>: U(O)"
+  Unit_form: "\<one>: U O"
 and
   Unit_intro: "\<star>: \<one>"
 and
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