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

---
 EqualProps.thy | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'EqualProps.thy')

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