diff options
| -rw-r--r-- | Equivalence.thy | 75 | ||||
| -rw-r--r-- | Prod.thy | 32 |
2 files changed, 83 insertions, 24 deletions
diff --git a/Equivalence.thy b/Equivalence.thy index b8df15d..07ef0df 100644 --- a/Equivalence.thy +++ b/Equivalence.thy @@ -74,9 +74,7 @@ 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: +schematic_goal composition_homl: assumes [intro]: "H: f ~[x: A. B] g" "f: A \<rightarrow> B" "g: A \<rightarrow> B" "h: B \<rightarrow> C" @@ -84,9 +82,21 @@ schematic_goal composition_homotopyl: 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+) + show "ap[h, B, C, f`x, g`x]`(H`x): h`(f`x) =[C] h`(g`x)" by (routine, fold homotopy_def, fact+) qed routine +schematic_goal composition_homr: + assumes [intro]: + "H: f ~[x: B. C] g" + "h: A \<rightarrow> B" "f: B \<rightarrow> C" "g: B \<rightarrow> C" + "A: U i" "B: U i" "C: U i" + shows "?prf: f o[A] h ~[x: A. C] g o[A] h" +unfolding homotopy_def compose_def proof (rule Prod_routine, subst (0 1) comp) + fix x assume [intro]: "x: A" + show "H`(h`x): f`(h`x) =[C] g`(h`x)" by (routine, fold homotopy_def, routine) +qed routine + + section \<open>Bi-invertibility\<close> definition biinv :: "[t, t, t] \<Rightarrow> t" ("(2biinv[_, _]/ _)") @@ -109,10 +119,10 @@ 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) +unfolding biinv_def proof (rule Sum_routine) 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 +qed derive definition equivalence :: "[t, t] \<Rightarrow> t" (infix "\<cong>" 100) where "A \<cong> B \<equiv> \<Sum>f: A \<rightarrow> B. biinv[A, B] f" @@ -135,22 +145,43 @@ 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 + +assume [intro]: "b: biinv[A, B] f" + +text \<open>Components of the witness of biinvertibility of @{term f}:\<close> + +let ?fst_of_b = + "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: B. B] id B]" +and ?snd_of_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: B. B] id B]" + +define g H g' H' where + "g \<equiv> fst[B \<rightarrow> A, \<lambda>g. g o[A] f ~[x: A. A] id A] ` (?fst_of_b ` b)" and + "H \<equiv> snd[B \<rightarrow> A, \<lambda>g. g o[A] f ~[x: A. A] id A] ` (?fst_of_b ` b)" and + "g' \<equiv> fst[B \<rightarrow> A, \<lambda>g. f o[B] g ~[x: B. B] id B] ` (?snd_of_b ` b)" and + "H' \<equiv> snd[B \<rightarrow> A, \<lambda>g. f o[B] g ~[x: B. B] id B] ` (?snd_of_b ` b)" + +have "H: g o[A] f ~[x: A. A] id A" +unfolding H_def g_def proof standard+ + have + "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: B. B] id B] : + (biinv[A, B] f) \<rightarrow> (\<Sum>(g: B \<rightarrow> A). g o[A] f ~[g: A. A] id A)" unfolding biinv_def by derive + thus + "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: B. B] id B]`b : + \<Sum>(g: B \<rightarrow> A). g o[A] f ~[g: A. A] id A" by derive rule +qed derive + +moreover have "(id A) o[B] g' \<equiv> g'" proof derive + show "g': B \<rightarrow> A" unfolding g'_def proof + have + "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: B. B] id B] : + (biinv[A, B] f) \<rightarrow> (\<Sum>(g: B \<rightarrow> A). f o[B] g ~[x: B. B] id B)" unfolding biinv_def by derive + thus + "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: B. B] id B]`b : + \<Sum>(g: B \<rightarrow> A). f o[B] g ~[x: B. B] id B" by derive rule + qed derive +qed + section \<open>Transport, homotopy, and bi-invertibility\<close> @@ -119,8 +119,36 @@ unfolding compose_def by (derive lems: assms cong) abbreviation id :: "t \<Rightarrow> t" ("(id _)" [115] 114) where "id A \<equiv> \<lambda>x: A. x" -lemma id_type [intro]: "\<And>A. A: U i \<Longrightarrow> id A: A \<rightarrow> A" by derive - +lemma id_type: "\<And>A. A: U i \<Longrightarrow> id A: A \<rightarrow> A" by derive + +lemma id_compl: + assumes [intro]: "A: U i" "B: U i" "f: A \<rightarrow> B" + shows "id B o[A] f \<equiv> f" +unfolding compose_def proof - + { + fix x assume [intro]: "x: A" + have "(id B)`(f`x) \<equiv> f`x" by derive + } + hence "\<lambda>x: A. (id B)`(f`x) \<equiv> \<lambda>x: A. f`x" by (derive lems: cong) derive + also have "\<lambda>x: A. f`x \<equiv> f" by derive + finally show "\<lambda>(x: A). (id B)`(f`x) \<equiv> f" by simp +qed + +lemma id_compr: + assumes [intro]: "A: U i" "B: U i" "f: A \<rightarrow> B" + shows "f o[A] id A \<equiv> f" +unfolding compose_def proof - + { + fix x assume [intro]: "x: A" + have "f`((id A)`x) \<equiv> f`x" by derive + } + hence "\<lambda>x: A. f`((id A)`x) \<equiv> \<lambda>x: A. f`x" by (derive lems: cong) derive + also have "\<lambda>x: A. f`x \<equiv> f" by derive + finally show "\<lambda>x: A. f`((id A)`x) \<equiv> f" by simp +qed + +declare id_type [intro] +lemmas id_comp [comp] = id_compl id_compr section \<open>Universal quantification\<close> |