From cd7609be19289fefe5404fce6a3fed4957ae7157 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 11 Sep 2018 15:40:37 +0200
Subject: Running into trouble with the polymorphic identity function

---
 EqualProps.thy | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'EqualProps.thy')

diff --git a/EqualProps.thy b/EqualProps.thy
index f00020f..0107e8e 100644
--- a/EqualProps.thy
+++ b/EqualProps.thy
@@ -275,7 +275,22 @@ sorry
 
 section \<open>Transport\<close>
 
+definition transport :: "Term \<Rightarrow> Term" where
+  "transport p \<equiv> ind\<^sub>= (\<lambda>x. (\<^bold>\<lambda>x. x)) p"
 
+lemma transport_type:
+  assumes
+    "A: U i" "P: A \<longrightarrow> U i"
+    "x: A" "y: A"
+    "p: x =\<^sub>A y"
+  shows "transport p: P x \<rightarrow> P y"
+unfolding transport_def
+by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (routine lems: assms)
+
+lemma transport_comp:
+  assumes "A: U i" and "x: A"
+  shows "transport (refl x) \<equiv> id"
+unfolding transport_def by (derive lems: assms)
 
 
 end
-- 
cgit v1.2.3