type lemmas for derived functions should type the functions themselves

1 files changed, 88 insertions, 21 deletions

diff --git a/Type_Families.thy b/Type_Families.thy
index f874e3d..6c784e5 100644
--- a/Type_Families.thy
+++ b/Type_Families.thy
@@ -2,7 +2,7 @@
 Isabelle/HoTT: Type families as fibrations
 Feb 2019
 
-Various results viewing type families as fibrations: transport, dependent map, path lifting etc.
+Various results viewing type families as fibrations: transport, path lifting, dependent map etc.
 
 ********)
 
@@ -41,8 +41,8 @@ end
 \<close>
 
 corollary transport_type:
-  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"
+  assumes [intro]: "A: U i" "P: A \<leadsto> U j" "x: A" "y: A"
+  shows "transport[A, P, x, y]: x =[A] y \<rightarrow> P x \<rightarrow> P y"
 unfolding transport_def by derive
 
 lemma transport_comp:
@@ -64,14 +64,14 @@ proof (path_ind' x y p)
   fix x assume [intro]: "x: A"
   show
   "refl (id 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"
+    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[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"
+  "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
 
@@ -91,8 +91,8 @@ proof (path_ind' x y p)
   
   fix y p assume [intro]: "y: A" "p: x =[A] y"
   show
-    "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"
+  "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
 
@@ -101,41 +101,108 @@ declare
   transport_invr [intro]
 
 
+section \<open>Path lifting\<close>
+
 schematic_goal path_lifting:
   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>"
+  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>"
+  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 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>"
+    "x: A" "y: A"
+  shows
+    "lift[A, P, x, y]:
+      \<Prod>u: P x. \<Prod>p: x =[A] y. <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:
+corollary lift_comp:
+  assumes [intro]:
+    "P: A \<leadsto> U i" "A: U i"
+    "x: A" "u: P x"
+  shows "lift[A, P, x, x]`u`(refl x) \<equiv> refl <x, u>"
+unfolding lift_def apply compute prefer 3 apply compute by derive
+
+declare
+  lift_type [intro]
+  lift_comp [comp]
+
+text \<open>
+Proof of the computation property of @{const lift}, stating that the first projection of the lift of @{term p} is equal to @{term p}:
+\<close>
+
+schematic_goal lift_fst_comp:
   assumes [intro]:
     "P: A \<leadsto> U i" "A: U i"
     "x: A" "y: A" "p: x =[A] y"
-    "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
+  defines
+    "Fst \<equiv> \<lambda>x y p u. ap[fst[A, P], \<Sum>x: A. P x, A, <x, u>, <y, transport[A, P, x, y]`p`u>]"
+  shows
+    "?prf: \<Prod>u: P x. (Fst x y p u)`(lift[A, P, x, y]`u`p) =[x =[A] y] p"
+proof
+  (path_ind' x y p, quantify_all)
+  fix x assume [intro]: "x: A"
+  show "\<And>u. u: P x \<Longrightarrow>
+    refl(refl x): (Fst x x (refl x) u)`(lift[A, P, x, x]`u`(refl x)) =[x =[A] x] refl x"
+  unfolding Fst_def by derive
+
+  fix y p assume [intro]: "y: A" "p: x =[A] y"
+  show "\<Prod>u: P x. (Fst x y p u)`(lift[A, \<lambda>a. P a, x, y]`u`p) =[x =[A] y] p: U i"
+  proof derive
+    fix u assume [intro]: "u: P x"
+    have
+      "fst[A, P]`<x, u> \<equiv> x" "fst[A, P]`<y, transport[A, P, x, y]`p`u> \<equiv> y" by derive
+    moreover have 
+      "Fst x y p u:
+        <x, u> =[\<Sum>(x: A). P x] <y, transport[A, P, x, y]`p`u> \<rightarrow>
+          fst[A, P]`<x, u> =[A] fst[A, P]`<y, transport[A, P, x, y]`p`u>"
+      unfolding Fst_def by derive
+    ultimately show
+      "Fst x y p u: <x, u> =[\<Sum>(x: A). P x] <y, transport[A, P, x, y]`p`u> \<rightarrow> x =[A] y"
+    by simp
+  qed routine
+qed fact
+
+
+section \<open>Dependent map\<close>
+
+schematic_goal dependent_map:
+  assumes [intro]:
+    "A: U i" "B: A \<leadsto> U i"
+    "f: \<Prod>x: A. B x"
+    "x: A" "y: A" "p: x =[A] y"
+  shows "?prf: transport[A, B, x, y]`p`(f`x) =[B y] f`y"
+proof (path_ind' x y p)
+  show "\<And>x. x: A \<Longrightarrow> refl (f`x): transport[A, B, x, x]`(refl x)`(f`x) =[B x] f`x" by derive
+qed derive
+
+definition apd :: "[t, t, t \<Rightarrow> t, t, t] \<Rightarrow> t"  ("(apd[_, _, _, _, _])") where
+"apd[f, A, B, x, y] \<equiv>
+  \<lambda>p: x =[A] y. indEq (\<lambda>x y p. transport[A, B, x, y]`p`(f`x) =[B y] f`y) (\<lambda>x. refl (f`x)) x y p"
+
+corollary apd_type:
+  assumes [intro]:
+    "A: U i" "B: A \<leadsto> U i"
+    "f: \<Prod>x: A. B x"
+    "x: A" "y: A"
+  shows "apd[f, A, B, x, y]: \<Prod>p: x =[A] y. transport[A, B, x, y]`p`(f`x) =[B y] f`y"
+unfolding apd_def by derive
+
+declare apd_type [intro]
 
 
 end