aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--Equivalence.thy197
-rw-r--r--HoTT_Methods.thy4
-rw-r--r--Prod.thy2
-rw-r--r--Projections.thy4
4 files changed, 202 insertions, 5 deletions
diff --git a/Equivalence.thy b/Equivalence.thy
new file mode 100644
index 0000000..b8df15d
--- /dev/null
+++ b/Equivalence.thy
@@ -0,0 +1,197 @@
+(********
+Isabelle/HoTT: Quasi-inverse and equivalence
+Mar 2019
+
+********)
+
+theory Equivalence
+imports Type_Families
+
+begin
+
+section \<open>Homotopy\<close>
+
+definition homotopy :: "[t, t \<Rightarrow> t, t, t] \<Rightarrow> t" ("(2homotopy[_, _] _ _)" [0, 0, 1000, 1000])
+where "homotopy[A, B] f g \<equiv> \<Prod>x: A. f`x =[B x] g`x"
+
+declare homotopy_def [comp]
+
+syntax "_homotopy" :: "[t, idt, t, t, t] \<Rightarrow> t" ("(1_ ~[_: _. _]/ _)" [101, 0, 0, 0, 101] 100)
+translations "f ~[x: A. B] g" \<rightleftharpoons> "(CONST homotopy) A (\<lambda>x. B) f g"
+
+lemma homotopy_type:
+ assumes [intro]: "A: U i" "B: A \<leadsto> U i" "f: \<Prod>x: A. B x" "g: \<Prod>x: A. B x"
+ shows "f ~[x: A. B x] g: U i"
+by derive
+
+declare homotopy_type [intro]
+
+text \<open>Homotopy inverse and composition (symmetry and transitivity):\<close>
+
+definition hominv :: "[t, t \<Rightarrow> t, t, t] \<Rightarrow> t" ("(2hominv[_, _, _, _])")
+where "hominv[A, B, f, g] \<equiv> \<lambda>H: f ~[x: A. B x] g. \<lambda>x: A. inv[B x, f`x, g`x]`(H`x)"
+
+lemma hominv_type:
+ assumes [intro]: "A: U i" "B: A \<leadsto> U i" "f: \<Prod>x: A. B x" "g: \<Prod>x: A. B x"
+ shows "hominv[A, B, f, g]: f ~[x: A. B x] g \<rightarrow> g ~[x: A. B x] f"
+unfolding hominv_def by (derive, fold homotopy_def)+ derive
+
+definition homcomp :: "[t, t \<Rightarrow> t, t, t, t] \<Rightarrow> t" ("(2homcomp[_, _, _, _, _])") where
+ "homcomp[A, B, f, g, h] \<equiv> \<lambda>H: f ~[x: A. B x] g. \<lambda>H': g ~[x: A. B x] h.
+ \<lambda>x: A. pathcomp[B x, f`x, g`x, h`x]`(H`x)`(H'`x)"
+
+lemma homcomp_type:
+ assumes [intro]:
+ "A: U i" "B: A \<leadsto> U i"
+ "f: \<Prod>x: A. B x" "g: \<Prod>x: A. B x" "h: \<Prod>x: A. B x"
+ shows "homcomp[A, B, f, g, h]: f ~[x: A. B x] g \<rightarrow> g ~[x: A. B x] h \<rightarrow> f ~[x: A. B x] h"
+unfolding homcomp_def by (derive, fold homotopy_def)+ derive
+
+schematic_goal fun_eq_imp_homotopy:
+ assumes [intro]:
+ "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"
+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]:
+ "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 "happly[x: A. B x] f g p: f ~[x: A. B x] g"
+unfolding happly_def by (derive lems: fun_eq_imp_homotopy)
+
+text \<open>Homotopy and function composition:\<close>
+
+declare[[pretty_compose=false]]
+
+schematic_goal composition_homotopyl:
+ assumes [intro]:
+ "H: f ~[x: A. B] g"
+ "f: A \<rightarrow> B" "g: A \<rightarrow> B" "h: B \<rightarrow> C"
+ "A: U i" "B: U i" "C: U i"
+ shows "?prf: h o[A] f ~[x: A. C] h o[A] g"
+unfolding homotopy_def compose_def proof (rule Prod_routine, subst (0 1) comp)
+ fix x assume [intro]: "x: A"
+ show "ap[h, B, C, f`x, g`x]`(H`x): h`(f`x) =[C] h`(g`x)" by (derive, fold homotopy_def, fact+)
+qed routine
+
+section \<open>Bi-invertibility\<close>
+
+definition biinv :: "[t, t, t] \<Rightarrow> t" ("(2biinv[_, _]/ _)")
+where "biinv[A, B] f \<equiv>
+ (\<Sum>g: B \<rightarrow> A. g o[A] f ~[x:A. A] id A) \<times> (\<Sum>g: B \<rightarrow> A. f o[B] g ~[x: B. B] id B)"
+
+text \<open>
+The meanings of the syntax defined above are:
+\<^item> @{term "f ~[x: A. B x] g"} expresses that @{term f} and @{term g} are homotopy functions of type @{term "\<Prod>x:A. B x"}.
+\<^item> @{term "biinv[A, B] f"} expresses that the function @{term f} of type @{term "A \<rightarrow> B"} is bi-invertible.
+\<close>
+
+lemma biinv_type:
+ assumes [intro]: "A: U i" "B: U i" "f: A \<rightarrow> B"
+ shows "biinv[A, B] f: U i"
+unfolding biinv_def by derive
+
+declare biinv_type [intro]
+
+schematic_goal id_is_biinv:
+ assumes [intro]: "A: U i"
+ shows "?prf: biinv[A, A] (id A)"
+unfolding biinv_def proof (rule Sum_routine, compute)
+ show "<id A, \<lambda>x: A. refl x>: \<Sum>(g: A \<rightarrow> A). (g o[A] id A) ~[x: A. A] (id A)" by derive
+ show "<id A, \<lambda>x: A. refl x>: \<Sum>(g: A \<rightarrow> A). (id A o[A] g) ~[x: A. A] (id A)" by derive
+qed routine
+
+definition equivalence :: "[t, t] \<Rightarrow> t" (infix "\<cong>" 100)
+where "A \<cong> B \<equiv> \<Sum>f: A \<rightarrow> B. biinv[A, B] f"
+
+schematic_goal equivalence_symmetric:
+ assumes [intro]: "A: U i"
+ shows "?prf: A \<cong> A"
+unfolding equivalence_def proof (rule Sum_routine)
+ show "\<And>f. f : A \<rightarrow> A \<Longrightarrow> biinv[A, A] f : U i" unfolding biinv_def by derive
+ show "id A: A \<rightarrow> A" by routine
+qed (routine add: id_is_biinv)
+
+
+section \<open>Quasi-inverse\<close>
+
+definition qinv :: "[t, t, t] \<Rightarrow> t" ("(2qinv[_, _]/ _)")
+where "qinv[A, B] f \<equiv> \<Sum>g: B \<rightarrow> A. (g o[A] f ~[x: A. A] id A) \<times> (f o[B] g ~[x: B. B] id B)"
+
+schematic_goal biinv_imp_qinv:
+ assumes [intro]: "A: U i" "B: U i" "f: A \<rightarrow> B"
+ shows "?prf: (biinv[A, B] f) \<rightarrow> (qinv[A,B] f)"
+proof (rule Prod_routine)
+assume "b: biinv[A, B] f"
+define g H g' H' where
+ "g \<equiv> fst[B \<rightarrow> A, \<lambda>g. g o[A] f ~[x: A. A] id A] `
+ (fst[\<Sum>g: B \<rightarrow> A. g o[A] f ~[x: A. A] id A, &(\<Sum>g: B \<rightarrow> A. f o[B] g ~[x: A. A] id B)] ` b)"
+and
+ "H \<equiv> snd[B \<rightarrow> A, \<lambda>g. g o[A] f ~[x: A. A] id A] `
+ (fst[\<Sum>g: B \<rightarrow> A. g o[A] f ~[x: A. A] id A, &(\<Sum>g: B \<rightarrow> A. f o[B] g ~[x: A. A] id B)] ` b)"
+and
+ "g' \<equiv> fst[B \<rightarrow> A, \<lambda>g. f o[B] g ~[x: B. B] id B] `
+ (snd[\<Sum>g: B \<rightarrow> A. g o[A] f ~[x: A. A] id A, &(\<Sum>g: B \<rightarrow> A. f o[B] g ~[x: A. A] id B)] ` b)"
+and
+ "H' \<equiv> snd[B \<rightarrow> A, \<lambda>g. f o[B] g ~[x: B. B] id B] `
+ (snd[\<Sum>g: B \<rightarrow> A. g o[A] f ~[x: A. A] id A, &(\<Sum>g: B \<rightarrow> A. f o[B] g ~[x: A. A] id B)] ` b)"
+
+have "g o[B] (f o[B] g') \<equiv> g"
+unfolding g_def g'_def proof compute
+
+
+section \<open>Transport, homotopy, and bi-invertibility\<close>
+
+schematic_goal transport_invl_hom:
+ assumes [intro]:
+ "P: A \<leadsto> U j" "A: U i"
+ "x: A" "y: A" "p: x =[A] y"
+ shows "?prf:
+ (transport[A, P, y, x]`(inv[A, x, y]`p)) o[P x] (transport[A, P, x, y]`p) ~[w: P x. P x] id P x"
+by (rule happly_type[OF transport_invl], derive)
+
+schematic_goal transport_invr_hom:
+ assumes [intro]:
+ "A: U i" "P: A \<leadsto> U j"
+ "y: A" "x: A" "p: x =[A] y"
+ shows "?prf:
+ (transport[A, P, x, y]`p) o[P y] (transport[A, P, y, x]`(inv[A, x, y]`p)) ~[w: P y. P y] id P y"
+by (rule happly_type[OF transport_invr], derive)
+
+declare
+ transport_invl_hom [intro]
+ transport_invr_hom [intro]
+
+text \<open>
+The following result states that the transport of an equality @{term p} is bi-invertible, with inverse given by the transport of the inverse @{text "~p"}.
+\<close>
+
+schematic_goal transport_biinv:
+ assumes [intro]: "p: A =[U i] B" "A: U i" "B: U i"
+ shows "?prf: biinv[A, B] (transport[U i, Id, A, B]`p)"
+unfolding biinv_def
+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)
+\<comment> \<open>The remaining subgoals are now handled easily\<close>
+by derive
+
+
+end
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index e45608e..0199a49 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -68,8 +68,8 @@ It also handles universes using @{method cumulativity}.
The method @{method hierarchy} has been observed to cause looping in previous versions, and is hence no longer part of @{theory_text derive}.
\<close>
-method derive uses lems declares comp =
- (routine add: lems | compute add: lems comp: comp | cumulativity form: lems)+
+method derive uses lems unfold declares comp =
+ (unfold unfold | routine add: lems | compute add: lems comp: comp | cumulativity form: lems)+
section \<open>Additional method combinators\<close>
diff --git a/Prod.thy b/Prod.thy
index aeddc49..75db657 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -15,7 +15,7 @@ section \<open>Basic type definitions\<close>
axiomatization
Prod :: "[t, t \<Rightarrow> t] \<Rightarrow> t" and
lam :: "[t, t \<Rightarrow> t] \<Rightarrow> t" and
- app :: "[t, t] \<Rightarrow> t" ("(2_`_)" [120, 121] 120)
+ app :: "[t, t] \<Rightarrow> t" ("(2_`/_)" [120, 121] 120)
\<comment> \<open>Application should bind tighter than abstraction.\<close>
syntax
diff --git a/Projections.thy b/Projections.thy
index a28c66b..c89b569 100644
--- a/Projections.thy
+++ b/Projections.thy
@@ -11,10 +11,10 @@ imports Prod Sum
begin
-definition fst ("(2fst[_, _])")
+definition fst ("(2fst[_,/ _])")
where "fst[A, B] \<equiv> \<lambda>(p: \<Sum>x: A. B x). indSum (\<lambda>_. A) (\<lambda>x y. x) p"
-definition snd ("(2snd[_, _])")
+definition snd ("(2snd[_,/ _])")
where "snd[A, B] \<equiv> \<lambda>(p: \<Sum>x: A. B x). indSum (\<lambda>p. B (fst[A, B]`p)) (\<lambda>x y. y) p"
lemma fst_type: