Removed transport section from Eq.thy

1 files changed, 1 insertions, 99 deletions

diff --git a/Eq.thy b/Eq.thy
index 8814c1f..9a7ba47 100644
--- a/Eq.thy
+++ b/Eq.thy
@@ -7,7 +7,7 @@ Intensional equality, path induction, and proofs of various results.
 ********)
 
 theory Eq
-imports Prod HoTT_Methods
+imports HoTT_Methods Prod
 
 begin
 
@@ -243,10 +243,6 @@ proof -
   by derive
 qed routine
 
-(* Todo, if possible:
-   Implement a custom version of schematic_goal/theorem that exports the derived proof term.
-*)
-
 
 section \<open>Functoriality of functions on types under equality\<close>
 
@@ -376,98 +372,4 @@ proof (path_ind' x y p)
 qed
 
 
-section \<open>Transport\<close>
-
-schematic_goal transport:
-  assumes [intro]:
-    "P: A \<rightarrow> U j" "A: U i"
-    "x: A" "y: A" "p: x =[A] y"
-  shows "?prf: P`x \<rightarrow> P`y"
-proof (path_ind' x y p)
-  show "\<And>x. x: A \<Longrightarrow> id P`x: P`x \<rightarrow> P`x" by derive
-qed routine
-
-definition transport :: "[t, t, t, t] \<Rightarrow> t"  ("(2transport[_, _, _] _)" [0, 0, 0, 1000])
-where "transport[P, x, y] p \<equiv> indEq (\<lambda>a b. & (P`a \<rightarrow> P`b)) (\<lambda>x. id P`x) x y p"
-
-syntax "_transport'" :: "[t, t] \<Rightarrow> t"  ("(2_*)" [1000])
-
-ML \<open>val pretty_transport = Attrib.setup_config_bool @{binding "pretty_transport"} (K true)\<close>
-
-print_translation \<open>
-let fun transport_tr' ctxt [P, x, y, p] =
-  if Config.get ctxt pretty_transport
-  then Syntax.const @{syntax_const "_transport'"} $ p
-  else @{const transport} $ P $ x $ y $ p
-in
-  [(@{const_syntax transport}, transport_tr')]
-end
-\<close>
-
-corollary transport_type:
-  assumes "P: A \<rightarrow> U j" "A: U i" "x: A" "y: A" "p: x =[A] y"
-  shows "transport[P, x, y] p: P`x \<rightarrow> P`y"
-unfolding transport_def using assms by (rule transport)
-
-lemma transport_comp:
-  assumes [intro]: "A: U i" "P: A \<rightarrow> U j" "a: A"
-  shows "transport P a a (refl a) \<equiv> id P`a"
-unfolding transport_def by derive
-
-declare
-  transport_type [intro]
-  transport_comp [comp]
-
-schematic_goal transport_invl:
-  assumes [intro]:
-    "A: U i" "P: A \<rightarrow> U j"
-    "x: A" "y: A" "p: x =[A] y"
-  shows "?prf:
-    (transport[P, y, x] (inv[A, x, y] p)) o[P`x] (transport[P, x, y] p) =[P`x \<rightarrow> P`x] id P`x"
-proof (path_ind' x y p)
-  fix x assume [intro]: "x: A"
-  show
-  "refl (id P`x) :
-    transport[P, x, x] (inv[A, x, x] (refl x)) o[P`x] (transport[P, x, x] (refl x)) =[P`x \<rightarrow> P`x]
-      id P`x"
-  by derive
-  
-  fix y p assume [intro]: "y: A" "p: x =[A] y"
-  have [intro]:
-    "transport[P, y, x] (inv[A, x, y] p) o[P`x] transport[P, x, y] p : P`x \<rightarrow> P`x"
-  proof show "transport[P, x, y] p: P`x \<rightarrow> P`y" by routine qed routine
-  
-  show
-    "transport[P, y, x] (inv[A, x, y] p) o[P`x] transport[P, x, y] p =[P`x \<rightarrow> P`x] id P`x: U j"
-  by derive
-qed
-
-schematic_goal transport_invr:
-  assumes [intro]:
-    "A: U i" "P: A \<rightarrow> U j"
-    "x: A" "y: A" "p: x =[A] y"
-  shows "?prf:
-    (transport[P, x, y] p) o[P`y] (transport[P, y, x] (inv[A, x, y] p)) =[P`y \<rightarrow> P`y] id P`y"
-proof (path_ind' x y p)
-  fix x assume [intro]: "x: A"
-  show
-  "refl (id P`x) :
-    (transport[P, x, x] (refl x)) o[P`x] transport[P, x, x] (inv[A, x, x] (refl x)) =[P`x \<rightarrow> P`x]
-      id P`x"
-  by derive
-  
-  fix y p assume [intro]: "y: A" "p: x =[A] y"
-  have [intro]:
-    "transport[P, x, y] p o[P`y] transport[P, y, x] (inv[A, x, y] p): P`y \<rightarrow> P`y"
-  proof show "transport[P, x, y] p: P`x \<rightarrow> P`y" by routine qed routine
-  
-  show
-    "transport[P, x, y] p o[P`y] transport[P, y, x] (inv[A, x, y] p) =[P`y \<rightarrow> P`y] id P`y: U j"
-  by derive
-qed
-
-declare
-  transport_invl [intro]
-  transport_invr [intro]
-
 end