Make functions object-level

1 files changed, 53 insertions, 27 deletions

diff --git a/Type_Families.thy b/Type_Families.thy
index b1e7686..f874e3d 100644
--- a/Type_Families.thy
+++ b/Type_Families.thy
@@ -7,7 +7,7 @@ Various results viewing type families as fibrations: transport, dependent map, p
 ********)
 
 theory Type_Families
-imports HoTT_Methods Sum Eq
+imports HoTT_Methods Sum Projections Eq
 
 begin
 
@@ -23,31 +23,31 @@ 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 \<Rightarrow> 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"
+definition transport :: "[t, t \<Rightarrow> t, t, t] \<Rightarrow> t"  ("(2transport[_, _, _, _])")
+where "transport[A, P, x, y] \<equiv> \<lambda>p: x =[A] y. 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])
+syntax "_transport'" :: "t \<Rightarrow> t"  ("transport[_]")
 
 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] =
+let fun transport_tr' ctxt [A, P, x, y] =
   if Config.get ctxt pretty_transport
-  then Syntax.const @{syntax_const "_transport'"} $ p
-  else @{const transport} $ P $ x $ y $ p
+  then Syntax.const @{syntax_const "_transport'"} $ P
+  else @{const transport} $ A $ P $ x $ y
 in
   [(@{const_syntax transport}, transport_tr')]
 end
 \<close>
 
 corollary transport_type:
-  assumes "A: U i" "P: A \<leadsto> U j" "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)
+  assumes [intro]: "A: U i" "P: A \<leadsto> U j" "x: A" "y: A" "p: x =[A] y"
+  shows "transport[A, P, x, y]`p: P x \<rightarrow> P y"
+unfolding transport_def by derive
 
 lemma transport_comp:
   assumes [intro]: "A: U i" "P: A \<leadsto> U j" "a: A"
-  shows "transport P a a (refl a) \<equiv> id P a"
+  shows "transport[A, P, a, a]`(refl a) \<equiv> id P a"
 unfolding transport_def by derive
 
 declare
@@ -56,59 +56,85 @@ declare
 
 schematic_goal transport_invl:
   assumes [intro]:
-    "P: A \<leadsto> U j" "A: U i"
+    "A: U i" "P: A \<leadsto> 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"
+    (transport[A, P, y, x]`(inv[A, x, y]`p)) o[P x] (transport[A, 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]
+    transport[A, P, x, x]`(inv[A, x, x]`(refl x)) o[P x] (transport[A, 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"
   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"
+    "transport[A, P, y, x]`(inv[A, x, y]`p) o[P x] transport[A, P, x, y]`p =[P x \<rightarrow> P x] id P x :
+      U j"
   by derive
 qed
 
 schematic_goal transport_invr:
   assumes [intro]:
-    "P: A \<leadsto> U j" "A: U i"
+    "A: U i" "P: A \<leadsto> 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"
+    (transport[A, P, x, y]`p) o[P y] (transport[A, 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"
+    (transport[A, P, x, x]`(refl x)) o[P x] transport[A, 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"
   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"
+    "transport[A, P, x, y]`p o[P y] transport[A, P, y, x]`(inv[A, x, y]`p) =[P y \<rightarrow> P y] id P y :
+      U j"
   by derive
 qed
 
-(* The two proofs above are rather brittle: the assumption "P: A \<leadsto> U j" needs to be put first
-   in order for the method derive to automatically work.
-*)
-
 declare
   transport_invl [intro]
   transport_invr [intro]
 
 
 schematic_goal path_lifting:
-  assumes
-    "A: U i" "P: A \<leadsto> U j"
+  assumes [intro]:
+    "P: A \<leadsto> U i" "A: U i"
+    "x: A" "y: A" "p: x =[A] y"
+  shows "?prf: \<Prod>u: P x. <x, u> =[\<Sum>x: A. P x] <y, (transport[A, P, x, y]`p)`u>"
+proof (path_ind' x y p, rule Prod_routine)
+  fix x u assume [intro]: "x: A" "u: P x"
+  have "(transport[A, P, x, x]`(refl x))`u \<equiv> u" by derive
+  thus "(refl <x, u>): <x, u> =[\<Sum>(x: A). P x] <x, (transport[A, P, x, x]`(refl x))`u>"
+    proof simp qed routine
+qed routine
+
+definition lift :: "[t, t \<Rightarrow> t, t, t] \<Rightarrow> t"  ("(2lift[_, _, _, _])")
+where
+  "lift[A, P, x, y] \<equiv> \<lambda>u: P x. \<lambda>p: x =[A] y. (indEq
+      (\<lambda>x y p. \<Prod>u: P x. <x, u> =[\<Sum>(x: A). P x] <y, (transport[A, P, x, y]`p)`u>)
+      (\<lambda>x. \<lambda>(u: P x). refl <x, u>) x y p)`u"
+
+corollary lift_type:
+  assumes [intro]:
+    "P: A \<leadsto> U i" "A: U i"
+    "x: A" "y: A" "p: x =[A] y"
     "u: P x"
+  shows "lift[A, P, x, y]`u`p: <x, u> =[\<Sum>x: A. P x] <y, (transport[A, P, x, y]`p)`u>"
+unfolding lift_def by (derive lems: path_lifting)
+
+schematic_goal lift_comp:
+  assumes [intro]:
+    "P: A \<leadsto> U i" "A: U i"
     "x: A" "y: A" "p: x =[A] y"
-  shows "?prf: <x, u> =[\<Sum>x: A. P x] <y, (transport[P, x, y] p)`u>"
+    "u: P x"
+  defines "Fst \<equiv> ap[fst[A, P], \<Sum>x: A. P x, A, <x, u>, <y, (transport[A, P, x, y]`p)`u>]"
+  shows "?prf: Fst`(lift[A, P, x, y]`u`p) =[x =[A] y] p"
+proof derive
 oops