diff options
Diffstat (limited to '')
| -rw-r--r-- | hott/Equivalence.thy | 34 | ||||
| -rw-r--r-- | hott/Identity.thy | 47 | ||||
| -rw-r--r-- | hott/Nat.thy | 14 |
3 files changed, 47 insertions, 48 deletions
diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy index 7d1f2b1..a57ed44 100644 --- a/hott/Equivalence.thy +++ b/hott/Equivalence.thy @@ -52,7 +52,7 @@ Lemma (def) hsym: shows "g ~ f" unfolding homotopy_def proof intro - fix x assume "x: A" then have "f x = g x" + fix x assuming "x: A" then have "f x = g x" by (htpy H) thus "g x = f x" by (rule pathinv) fact @@ -70,7 +70,7 @@ Lemma (def) htrans: shows "f ~ h" unfolding homotopy_def proof intro - fix x assume "x: A" + fix x assuming "x: A" have *: "f x = g x" "g x = h x" by (htpy H1, htpy H2) show "f x = h x" @@ -119,7 +119,7 @@ Lemma funcomp_right_htpy: shows "(g \<circ> f) ~ (g \<circ> f')" unfolding homotopy_def proof (intro, reduce) - fix x assume "x: A" + fix x assuming "x: A" have *: "f x = f' x" by (htpy H) show "g (f x) = g (f' x)" @@ -154,18 +154,18 @@ Corollary (def) commute_homotopy': "H: f ~ (id A)" shows "H (f x) = f [H x]" proof - - from \<open>H: f ~ id A\<close> have "H: \<Prod>x: A. f x = x" + from \<open>H: f ~ id A\<close> have [type]: "H: \<Prod>x: A. f x = x" by (reduce add: homotopy_def) - have "(id A)[H x]: f x = x" + have *: "(id A)[H x]: f x = x" by (rewrite at "\<hole> = _" id_comp[symmetric], rewrite at "_ = \<hole>" id_comp[symmetric]) have "H (f x) \<bullet> H x = H (f x) \<bullet> (id A)[H x]" - by (rule left_whisker, transport eq: ap_id) (reduce+, refl) + by (rule left_whisker, fact *, transport eq: ap_id) (reduce+, refl) also have [simplified id_comp]: "H (f x) \<bullet> (id A)[H x] = f[H x] \<bullet> H x" by (rule commute_homotopy) - finally have *: "{}" by this + finally have *: "{}" using * by this show "H (f x) = f [H x]" by pathcomp_cancelr (fact, typechk+) @@ -179,7 +179,7 @@ subsection \<open>Quasi-inverses\<close> definition "is_qinv A B f \<equiv> \<Sum>g: B \<rightarrow> A. homotopy A (fn _. A) (g \<circ>\<^bsub>A\<^esub> f) (id A) \<times> homotopy B (fn _. B) (f \<circ>\<^bsub>B\<^esub> g) (id B)" -lemma is_qinv_type [type]: +Lemma is_qinv_type [type]: assumes "A: U i" "B: U i" "f: A \<rightarrow> B" shows "is_qinv A B f: U i" unfolding is_qinv_def @@ -266,7 +266,7 @@ definition "is_biinv A B f \<equiv> (\<Sum>g: B \<rightarrow> A. homotopy A (fn _. A) (g \<circ>\<^bsub>A\<^esub> f) (id A)) \<times> (\<Sum>g: B \<rightarrow> A. homotopy B (fn _. B) (f \<circ>\<^bsub>B\<^esub> g) (id B))" -lemma is_biinv_type [type]: +Lemma is_biinv_type [type]: assumes "A: U i" "B: U i" "f: A \<rightarrow> B" shows "is_biinv A B f: U i" unfolding is_biinv_def by typechk @@ -365,7 +365,7 @@ text \<open> definition equivalence (infix "\<simeq>" 110) where "A \<simeq> B \<equiv> \<Sum>f: A \<rightarrow> B. Equivalence.is_biinv A B f" -lemma equivalence_type [type]: +Lemma equivalence_type [type]: assumes "A: U i" "B: U i" shows "A \<simeq> B: U i" unfolding equivalence_def by typechk @@ -432,28 +432,24 @@ Lemma (def) equiv_if_equal: \<^enum> vars A B apply (rewrite at A in "A \<rightarrow> B" id_comp[symmetric]) using [[solve_side_conds=1]] - apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric], fact) + apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric]) apply (rule transport, rule Ui_in_USi) - apply (rule lift_universe_codomain, rule Ui_in_USi) - apply (typechk, rule Ui_in_USi) - by facts + by (rule lift_universe_codomain, rule Ui_in_USi) \<^enum> vars A using [[solve_side_conds=1]] apply (subst transport_comp) \<circ> by (rule Ui_in_USi) \<circ> by reduce (rule in_USi_if_in_Ui) - \<circ> by reduce (rule id_is_biinv, fact) + \<circ> by reduce (rule id_is_biinv) done done \<^item> \<comment> \<open>Similar proof as in the first subgoal above\<close> apply (rewrite at A in "A \<rightarrow> B" id_comp[symmetric]) using [[solve_side_conds=1]] - apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric], fact) + apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric]) apply (rule transport, rule Ui_in_USi) - apply (rule lift_universe_codomain, rule Ui_in_USi) - apply (typechk, rule Ui_in_USi) - by facts + by (rule lift_universe_codomain, rule Ui_in_USi) done (*Uncomment this to see all implicits from here on. diff --git a/hott/Identity.thy b/hott/Identity.thy index 4829b6f..247d6a4 100644 --- a/hott/Identity.thy +++ b/hott/Identity.thy @@ -82,7 +82,7 @@ Lemma (def) pathinv: shows "y =\<^bsub>A\<^esub> x" by (eq p) intro -lemma pathinv_comp [comp]: +Lemma pathinv_comp [comp]: assumes "A: U i" "x: A" shows "pathinv A x x (refl x) \<equiv> refl x" unfolding pathinv_def by reduce @@ -94,11 +94,11 @@ Lemma (def) pathcomp: shows "x =\<^bsub>A\<^esub> z" proof (eq p) - fix x q assume "x: A" and "q: x =\<^bsub>A\<^esub> z" + fix x q assuming "x: A" and "q: x =\<^bsub>A\<^esub> z" show "x =\<^bsub>A\<^esub> z" by (eq q) refl qed -lemma pathcomp_comp [comp]: +Lemma pathcomp_comp [comp]: assumes "A: U i" "a: A" shows "pathcomp A a a a (refl a) (refl a) \<equiv> refl a" unfolding pathcomp_def by reduce @@ -491,9 +491,9 @@ Lemma (def) right_whisker: shows "p \<bullet> r = q \<bullet> r" apply (eq r) focus vars x s t proof - - have "t \<bullet> refl x = t" by (rule pathcomp_refl) - also have ".. = s" by fact - also have ".. = s \<bullet> refl x" by (rule pathcomp_refl[symmetric]) + have "s \<bullet> refl x = s" by (rule pathcomp_refl) + also have ".. = t" by fact + also have ".. = t \<bullet> refl x" by (rule pathcomp_refl[symmetric]) finally show "{}" by this qed done @@ -505,9 +505,9 @@ Lemma (def) left_whisker: shows "r \<bullet> p = r \<bullet> q" apply (eq r) focus vars x s t proof - - have "refl x \<bullet> t = t" by (rule refl_pathcomp) - also have ".. = s" by fact - also have ".. = refl x \<bullet> s" by (rule refl_pathcomp[symmetric]) + have "refl x \<bullet> s = s" by (rule refl_pathcomp) + also have ".. = t" by fact + also have ".. = refl x \<bullet> t" by (rule refl_pathcomp[symmetric]) finally show "{}" by this qed done @@ -542,14 +542,13 @@ text \<open>Conditions under which horizontal path-composition is defined.\<clos locale horiz_pathcomposable = fixes i A a b c p q r s -assumes assums: +assumes [type]: "A: U i" "a: A" "b: A" "c: A" "p: a =\<^bsub>A\<^esub> b" "q: a =\<^bsub>A\<^esub> b" "r: b =\<^bsub>A\<^esub> c" "s: b =\<^bsub>A\<^esub> c" begin Lemma (def) horiz_pathcomp: - notes assums assumes "\<alpha>: p = q" "\<beta>: r = s" shows "p \<bullet> r = q \<bullet> s" proof (rule pathcomp) @@ -560,7 +559,6 @@ qed typechk text \<open>A second horizontal composition:\<close> Lemma (def) horiz_pathcomp': - notes assums assumes "\<alpha>: p = q" "\<beta>: r = s" shows "p \<bullet> r = q \<bullet> s" proof (rule pathcomp) @@ -572,13 +570,12 @@ notation horiz_pathcomp (infix "\<star>" 121) notation horiz_pathcomp' (infix "\<star>''" 121) Lemma (def) horiz_pathcomp_eq_horiz_pathcomp': - notes assums assumes "\<alpha>: p = q" "\<beta>: r = s" shows "\<alpha> \<star> \<beta> = \<alpha> \<star>' \<beta>" unfolding horiz_pathcomp_def horiz_pathcomp'_def apply (eq \<alpha>, eq \<beta>) focus vars p apply (eq p) - focus vars a q by (eq q) (reduce, refl) + focus vars a _ _ _ r by (eq r) (reduce, refl) done done @@ -597,7 +594,7 @@ Lemma \<Omega>2_alt_def: section \<open>Eckmann-Hilton\<close> -context fixes i A a assumes "A: U i" "a: A" +context fixes i A a assumes [type]: "A: U i" "a: A" begin interpretation \<Omega>2: @@ -619,14 +616,18 @@ Lemma (def) pathcomp_eq_horiz_pathcomp: assumes "\<alpha>: \<Omega>2 A a" "\<beta>: \<Omega>2 A a" shows "\<alpha> \<bullet> \<beta> = \<alpha> \<star> \<beta>" unfolding \<Omega>2.horiz_pathcomp_def - using assms[unfolded \<Omega>2_alt_def] + (*FIXME: Definitional unfolding + normalization; shouldn't need explicit + unfolding*) + using assms[unfolded \<Omega>2_alt_def, type] proof (reduce, rule pathinv) \<comment> \<open>Propositional equality rewriting needs to be improved\<close> - have "{} = refl (refl a) \<bullet> \<alpha>" by (rule pathcomp_refl) + have "refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a) = refl (refl a) \<bullet> \<alpha>" + by (rule pathcomp_refl) also have ".. = \<alpha>" by (rule refl_pathcomp) finally have eq\<alpha>: "{} = \<alpha>" by this - have "{} = refl (refl a) \<bullet> \<beta>" by (rule pathcomp_refl) + have "refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a) = refl (refl a) \<bullet> \<beta>" + by (rule pathcomp_refl) also have ".. = \<beta>" by (rule refl_pathcomp) finally have eq\<beta>: "{} = \<beta>" by this @@ -640,13 +641,15 @@ Lemma (def) pathcomp_eq_horiz_pathcomp': assumes "\<alpha>: \<Omega>2 A a" "\<beta>: \<Omega>2 A a" shows "\<alpha> \<star>' \<beta> = \<beta> \<bullet> \<alpha>" unfolding \<Omega>2.horiz_pathcomp'_def - using assms[unfolded \<Omega>2_alt_def] + using assms[unfolded \<Omega>2_alt_def, type] proof reduce - have "{} = refl (refl a) \<bullet> \<beta>" by (rule pathcomp_refl) + have "refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a) = refl (refl a) \<bullet> \<beta>" + by (rule pathcomp_refl) also have ".. = \<beta>" by (rule refl_pathcomp) finally have eq\<beta>: "{} = \<beta>" by this - have "{} = refl (refl a) \<bullet> \<alpha>" by (rule pathcomp_refl) + have "refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a) = refl (refl a) \<bullet> \<alpha>" + by (rule pathcomp_refl) also have ".. = \<alpha>" by (rule refl_pathcomp) finally have eq\<alpha>: "{} = \<alpha>" by this @@ -659,7 +662,7 @@ Lemma (def) pathcomp_eq_horiz_pathcomp': Lemma (def) eckmann_hilton: assumes "\<alpha>: \<Omega>2 A a" "\<beta>: \<Omega>2 A a" shows "\<alpha> \<bullet> \<beta> = \<beta> \<bullet> \<alpha>" - using assms[unfolded \<Omega>2_alt_def] + using assms[unfolded \<Omega>2_alt_def, type] proof - have "\<alpha> \<bullet> \<beta> = \<alpha> \<star> \<beta>" by (rule pathcomp_eq_horiz_pathcomp) diff --git a/hott/Nat.thy b/hott/Nat.thy index 716703a..f45387c 100644 --- a/hott/Nat.thy +++ b/hott/Nat.thy @@ -62,17 +62,17 @@ subsection \<open>Addition\<close> definition add (infixl "+" 120) where "m + n \<equiv> NatRec Nat m (K suc) n" -lemma add_type [type]: +Lemma add_type [type]: assumes "m: Nat" "n: Nat" shows "m + n: Nat" unfolding add_def by typechk -lemma add_zero [comp]: +Lemma add_zero [comp]: assumes "m: Nat" shows "m + 0 \<equiv> m" unfolding add_def by reduce -lemma add_suc [comp]: +Lemma add_suc [comp]: assumes "m: Nat" "n: Nat" shows "m + suc n \<equiv> suc (m + n)" unfolding add_def by reduce @@ -123,22 +123,22 @@ subsection \<open>Multiplication\<close> definition mul (infixl "*" 121) where "m * n \<equiv> NatRec Nat 0 (K $ add m) n" -lemma mul_type [type]: +Lemma mul_type [type]: assumes "m: Nat" "n: Nat" shows "m * n: Nat" unfolding mul_def by typechk -lemma mul_zero [comp]: +Lemma mul_zero [comp]: assumes "n: Nat" shows "n * 0 \<equiv> 0" unfolding mul_def by reduce -lemma mul_one [comp]: +Lemma mul_one [comp]: assumes "n: Nat" shows "n * 1 \<equiv> n" unfolding mul_def by reduce -lemma mul_suc [comp]: +Lemma mul_suc [comp]: assumes "m: Nat" "n: Nat" shows "m * suc n \<equiv> m + m * n" unfolding mul_def by reduce |