transport and homotopy

1 files changed, 80 insertions, 21 deletions

diff --git a/Univalence.thy b/Univalence.thy
index e073e50..04e1d67 100644
--- a/Univalence.thy
+++ b/Univalence.thy
@@ -20,6 +20,7 @@ declare homotopic_def [comp]
 syntax "_homotopic" :: "[t, idt, t, t, t] \<Rightarrow> t"  ("(1_ ~[_: _. _]/ _)" [101, 0, 0, 0, 101] 100)
 translations "f ~[x: A. B] g" \<rightleftharpoons> "(CONST homotopic) A (\<lambda>x. B) f g"
 
+(*
 syntax "_homotopic'" :: "[t, t] \<Rightarrow> t"  ("(2_ ~ _)" [1000, 1000])
 
 ML \<open>val pretty_homotopic = Attrib.setup_config_bool @{binding "pretty_homotopic"} (K true)\<close>
@@ -33,6 +34,7 @@ in
   [(@{const_syntax homotopic}, homotopic_tr')]
 end
 \<close>
+*)
 
 lemma homotopic_type:
   assumes [intro]: "A: U i" "B: A \<leadsto> U i" "f: \<Prod>x: A. B x" "g: \<Prod>x: A. B x"
@@ -43,26 +45,59 @@ declare homotopic_type [intro]
 
 schematic_goal fun_eq_imp_homotopic:
   assumes [intro]:
-    "A: U i" "B: A \<leadsto> U i"
-    "f: \<Prod>x: A. B x" "g: \<Prod>x: A. B x"
     "p: f =[\<Prod>x: A. B x] g"
+    "f: \<Prod>x: A. B x" "g: \<Prod>x: A. B x"
+    "A: U i" "B: A \<leadsto> U i"
   shows "?prf: f ~[x: A. B x] g"
 proof (path_ind' f g p)
   show "\<And>f. f : \<Prod>(x: A). B x \<Longrightarrow> \<lambda>x: A. refl(f`x): f ~[x: A. B x] f" by derive
 qed routine
 
-definition happly :: "[t, t \<Rightarrow> t, t, t, t] \<Rightarrow> t"  ("(2happly[_, _] _ _ _)" [0, 0, 1000, 1000, 1000])
-where "happly[A, B] f g p \<equiv> indEq (\<lambda>f g. & f ~[x: A. B x] g) (\<lambda>f. \<lambda>(x: A). refl(f`x)) f g p"
+definition happly :: "[t, t \<Rightarrow> t, t, t, t] \<Rightarrow> t"
+where "happly A B f g p \<equiv> indEq (\<lambda>f g. & f ~[x: A. B x] g) (\<lambda>f. \<lambda>(x: A). refl(f`x)) f g p"
+
+syntax "_happly" :: "[idt, t, t, t, t, t] \<Rightarrow> t"
+  ("(2happly[_: _. _] _ _ _)" [0, 0, 0, 1000, 1000, 1000])
+translations "happly[x: A. B] f g p"  \<rightleftharpoons> "(CONST happly) A (\<lambda>x. B) f g p"
 
 corollary happly_type:
   assumes [intro]:
-    "A: U i" "B: A \<leadsto> U i"
-    "f: \<Prod>x: A. B x" "g: \<Prod>x: A. B x"
     "p: f =[\<Prod>x: A. B x] g"
-  shows "happly[A, B] f g p: f ~[x: A. B x] g"
+    "f: \<Prod>x: A. B x" "g: \<Prod>x: A. B x"
+    "A: U i" "B: A \<leadsto> U i"
+  shows "happly[x: A. B x] f g p: f ~[x: A. B x] g"
 unfolding happly_def by (derive lems: fun_eq_imp_homotopic)
 
 
+section \<open>Transport and homotopy\<close>
+
+schematic_goal transport_invl_hom:
+  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) ~[w: P`x. P`x] id(P`x)"
+proof (rule happly_type[OF transport_invl])
+  show "(transport[P, y, x] (inv[A, x, y] p)) o[P`x] (transport[P, x, y] p): P`x \<rightarrow> P`x"
+  proof show "P`y: U j" by routine qed routine
+qed routine
+
+schematic_goal transport_invr_hom:
+  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)) ~[w: P`y. P`y] id(P`y)"
+proof (rule happly_type[OF transport_invr])
+  show "(transport[P, x, y] p) o[P`y] (transport[P, y, x] (inv[A, x, y] p)): P`y \<rightarrow> P`y"
+  proof show "P`x: U j" by routine qed routine
+qed routine
+
+declare
+  transport_invl_hom [intro]
+  transport_invr_hom [intro]
+
+
 section \<open>Equivalence\<close>
 
 text \<open>For now, we define equivalence in terms of bi-invertibility.\<close>
@@ -106,23 +141,47 @@ qed (routine add: id_is_biinv)
 
 section \<open>Univalence\<close>
 
-(*
+declare[[goals_limit=100, pretty_transport=true]]
+
+lemma lem: "\<And>A. A: U i \<Longrightarrow> (id (U i))`A \<equiv> A" by derive
+
 schematic_goal
   assumes [intro]: "A: U i" "B: U i" "p: A =[U i] B"
   shows "?prf: biinv[A, B] (transport[id(U i), A, B] p)"
+apply (path_ind' A B p)
+apply (unfold biinv_def)
+  show "?a : biinv[A, B] (transport[id(U i), A, B] p)"
+
+oops
+
+schematic_goal
+  assumes [intro]: "A: U i" "B: U i" "p: A =[U i] B"
+  shows "?prf: biinv[id(U i)`A, id(U i)`B] (transport[id(U i), A, B] p)"
 unfolding biinv_def
-apply (rule Sum_routine) defer
-apply (rule Sum_intro)
-  have
-    "transport[id(U i), A, B] p: (id (U i))`A \<rightarrow> (id (U i))`B"
-    by (derive lems: transport_type[where ?A="U i"]
-  moreover have
-    "(id (U i))`A \<rightarrow> (id (U i))`B \<equiv> A \<rightarrow> B" by deriv
-  ultimately have [intro]:
-    "transport[id(U i), A, B] p: A \<rightarrow> B" by simp
-
-  show "\<Sum>g: B \<rightarrow> A. (transport[id(U i), A, B] p o[B] g) ~[x: B. B] (id B) : U i"
-  by deriv
+apply (rule Sum_routine)
+prefer 2 apply (rule Sum_routine)
+prefer 3 apply (rule transport_invl_hom)
+prefer 9 apply (rule Sum_routine)
+prefer 3 apply (rule transport_invr_hom)
+proof -
+  show "U i: U (Suc i)" by hierarchy
+  show "U i: U (Suc i)" by hierarchy
+  show "\<And>g. g : id (U i)`B \<rightarrow> id (U i)`A \<Longrightarrow> (transport[id(U i), A, B] p) o[id (U i)`B] g ~[x: id (U i)`B. id (U i)`B] id (id (U i)`B) : U i"
+  proof
+    show "id (U i)`B : U i" by derive
+    show "id (U i)`B : U i" by derive
+    show "id (id (U i)`B) : id (U i)`B \<rightarrow> id (U i)`B" by derive
+    show
+      "\<And>g. g : id (U i)`B \<rightarrow> id (U i)`A \<Longrightarrow>
+        (transport[id(U i), A, B] p) o[id (U i)`B] g: id (U i)`B \<rightarrow> id (U i)`B"
+    apply rule
+    prefer 4 apply assumption
+    proof -
+      show "id (U i)`B : U i" by derive
+      show "id (U i)`A : U i" by derive
+      show "id (U i)`B : U i" by derive
+    
+oops
     
 
 schematic_goal type_eq_imp_equiv:
@@ -148,7 +207,7 @@ prefer 2
   qed fact+
 qed (derive lems: assms
 
-
+(*
 section \<open>The univalence axiom\<close>
 
 axiomatization univalence :: "[t, t] \<Rightarrow> t" where UA: "univalence A B: isequiv[A, B] idtoeqv"