diff options
Diffstat (limited to 'hott')
| -rw-r--r-- | hott/Equivalence.thy | 48 | ||||
| -rw-r--r-- | hott/Identity.thy | 47 | ||||
| -rw-r--r-- | hott/List+.thy | 4 |
3 files changed, 26 insertions, 73 deletions
diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy index a57ed44..99300a0 100644 --- a/hott/Equivalence.thy +++ b/hott/Equivalence.thy @@ -144,8 +144,6 @@ Lemma (def) commute_homotopy: apply (transport eq: pathcomp_refl, transport eq: refl_pathcomp) by refl -\<comment> \<open>TODO: *Really* need normalization during type-checking and better equality - type rewriting to do the proof below properly\<close> Corollary (def) commute_homotopy': assumes "A: U i" @@ -154,21 +152,18 @@ Corollary (def) commute_homotopy': "H: f ~ (id A)" shows "H (f x) = f [H x]" proof - + (*FIXME: Bug; if the following type declaration isn't made then bad things + happen on the next lines.*) 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" - 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, fact *, transport eq: ap_id) (reduce+, refl) + by (rule left_whisker, transport eq: ap_id, 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 *: "{}" using * by this + finally have "{}" by this - show "H (f x) = f [H x]" - by pathcomp_cancelr (fact, typechk+) + thus "H (f x) = f [H x]" by pathcomp_cancelr (fact, typechk+) qed @@ -309,23 +304,11 @@ Lemma (def) is_qinv_if_is_biinv: assumes "A: U i" "B: U i" "f: A \<rightarrow> B" shows "is_biinv f \<rightarrow> is_qinv f" apply intro - - text \<open>Split the hypothesis \<^term>\<open>is_biinv f\<close> into its components and name them.\<close> unfolding is_biinv_def apply elims focus vars _ _ _ g H1 h H2 - text \<open>Need to give the required function and homotopies.\<close> apply (rule is_qinvI) - text \<open>We claim that \<^term>\<open>g\<close> is a quasi-inverse to \<^term>\<open>f\<close>.\<close> \<^item> by (fact \<open>g: _\<close>) - - text \<open>The first part \<^prop>\<open>?H1: g \<circ> f ~ id A\<close> is given by \<^term>\<open>H1\<close>.\<close> \<^item> by (fact \<open>H1: _\<close>) - - text \<open> - It remains to prove \<^prop>\<open>?H2: f \<circ> g ~ id B\<close>. First show that \<open>g ~ h\<close>, - then the result follows from @{thm \<open>H2: f \<circ> h ~ id B\<close>}. Here a proof - block is used for calculational reasoning. - \<close> \<^item> proof - have "g ~ g \<circ> (id B)" by reduce refl also have ".. ~ g \<circ> f \<circ> h" by rhtpy (rule \<open>H2:_\<close>[symmetric]) @@ -437,7 +420,7 @@ Lemma (def) equiv_if_equal: by (rule lift_universe_codomain, rule Ui_in_USi) \<^enum> vars A using [[solve_side_conds=1]] - apply (subst transport_comp) + apply (rewrite transport_comp) \<circ> by (rule Ui_in_USi) \<circ> by reduce (rule in_USi_if_in_Ui) \<circ> by reduce (rule id_is_biinv) @@ -452,24 +435,5 @@ Lemma (def) equiv_if_equal: by (rule lift_universe_codomain, rule Ui_in_USi) done -(*Uncomment this to see all implicits from here on. -no_translations - "f x" \<leftharpoondown> "f `x" - "x = y" \<leftharpoondown> "x =\<^bsub>A\<^esub> y" - "g \<circ> f" \<leftharpoondown> "g \<circ>\<^bsub>A\<^esub> f" - "p\<inverse>" \<leftharpoondown> "CONST pathinv A x y p" - "p \<bullet> q" \<leftharpoondown> "CONST pathcomp A x y z p q" - "fst" \<leftharpoondown> "CONST Spartan.fst A B" - "snd" \<leftharpoondown> "CONST Spartan.snd A B" - "f[p]" \<leftharpoondown> "CONST ap A B x y f p" - "trans P p" \<leftharpoondown> "CONST transport A P x y p" - "trans_const B p" \<leftharpoondown> "CONST transport_const A B x y p" - "lift P p u" \<leftharpoondown> "CONST pathlift A P x y p u" - "apd f p" \<leftharpoondown> "CONST Identity.apd A P f x y p" - "f ~ g" \<leftharpoondown> "CONST homotopy A B f g" - "is_qinv f" \<leftharpoondown> "CONST Equivalence.is_qinv A B f" - "is_biinv f" \<leftharpoondown> "CONST Equivalence.is_biinv A B f" -*) - end diff --git a/hott/Identity.thy b/hott/Identity.thy index 247d6a4..dc27ee8 100644 --- a/hott/Identity.thy +++ b/hott/Identity.thy @@ -242,7 +242,7 @@ Lemma (def) ap_funcomp: "x: A" "y: A" "f: A \<rightarrow> B" "g: B \<rightarrow> C" "p: x = y" - shows "(g \<circ> f)[p] = g[f[p]]" thm ap + shows "(g \<circ> f)[p] = g[f[p]]" apply (eq p) \<^item> by reduce \<^item> by reduce refl @@ -251,10 +251,7 @@ Lemma (def) ap_funcomp: Lemma (def) ap_id: assumes "A: U i" "x: A" "y: A" "p: x = y" shows "(id A)[p] = p" - apply (eq p) - \<^item> by reduce - \<^item> by reduce refl - done + by (eq p) (reduce, refl) section \<open>Transport\<close> @@ -303,7 +300,7 @@ Lemma (def) pathcomp_cancel_left: by (transport eq: inv_pathcomp, transport eq: refl_pathcomp) refl also have ".. = p\<inverse> \<bullet> (p \<bullet> r)" by (transport eq: pathcomp_assoc[symmetric], transport eq: \<open>\<alpha>:_\<close>) refl - also have ".. = r" thm inv_pathcomp + also have ".. = r" by (transport eq: pathcomp_assoc, transport eq: inv_pathcomp, transport eq: refl_pathcomp) refl @@ -339,7 +336,7 @@ Lemma (def) transport_left_inv: "x: A" "y: A" "p: x = y" shows "(trans P p\<inverse>) \<circ> (trans P p) = id (P x)" - by (eq p) (reduce; refl) + by (eq p) (reduce, refl) Lemma (def) transport_right_inv: assumes @@ -440,10 +437,7 @@ Lemma (def) pathlift_fst: "u: P x" "p: x = y" shows "fst[lift P p u] = p" - apply (eq p) - \<^item> by reduce - \<^item> by reduce refl - done + by (eq p) (reduce, refl) section \<open>Dependent paths\<close> @@ -585,10 +579,10 @@ end section \<open>Loop space\<close> definition \<Omega> where "\<Omega> A a \<equiv> a =\<^bsub>A\<^esub> a" -definition \<Omega>2 where "\<Omega>2 A a \<equiv> \<Omega> (\<Omega> A a) (refl a)" +definition \<Omega>2 where "\<Omega>2 A a \<equiv> refl a =\<^bsub>a =\<^bsub>A\<^esub> a\<^esub> refl a" -Lemma \<Omega>2_alt_def: - "\<Omega>2 A a \<equiv> refl a = refl a" +Lemma \<Omega>2_\<Omega>_of_\<Omega>: + "\<Omega>2 A a \<equiv> \<Omega> (\<Omega> A a) (refl a)" unfolding \<Omega>2_def \<Omega>_def . @@ -604,23 +598,20 @@ interpretation \<Omega>2: notation \<Omega>2.horiz_pathcomp (infix "\<star>" 121) notation \<Omega>2.horiz_pathcomp' (infix "\<star>''" 121) -Lemma [type]: +Lemma assumes "\<alpha>: \<Omega>2 A a" and "\<beta>: \<Omega>2 A a" - shows horiz_pathcomp_type: "\<alpha> \<star> \<beta>: \<Omega>2 A a" - and horiz_pathcomp'_type: "\<alpha> \<star>' \<beta>: \<Omega>2 A a" + shows horiz_pathcomp_type [type]: "\<alpha> \<star> \<beta>: \<Omega>2 A a" + and horiz_pathcomp'_type [type]: "\<alpha> \<star>' \<beta>: \<Omega>2 A a" using assms - unfolding \<Omega>2.horiz_pathcomp_def \<Omega>2.horiz_pathcomp'_def \<Omega>2_alt_def + unfolding \<Omega>2.horiz_pathcomp_def \<Omega>2.horiz_pathcomp'_def \<Omega>2_def by reduce+ 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 - (*FIXME: Definitional unfolding + normalization; shouldn't need explicit - unfolding*) - using assms[unfolded \<Omega>2_alt_def, type] + using assms[unfolded \<Omega>2_def, type] (*TODO: A `noting` keyword that puts the noted theorem into [type]*) proof (reduce, rule pathinv) - \<comment> \<open>Propositional equality rewriting needs to be improved\<close> 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) @@ -641,7 +632,7 @@ 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, type] + using assms[unfolded \<Omega>2_def, type] proof reduce have "refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a) = refl (refl a) \<bullet> \<beta>" by (rule pathcomp_refl) @@ -662,20 +653,18 @@ 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, type] + using \<Omega>2_def[comp] proof - have "\<alpha> \<bullet> \<beta> = \<alpha> \<star> \<beta>" by (rule pathcomp_eq_horiz_pathcomp) also have [simplified comp]: ".. = \<alpha> \<star>' \<beta>" - \<comment> \<open>Danger, Will Robinson! (Inferred implicit has an equivalent form but - needs to be manually simplified.)\<close> + \<comment> \<open>Danger! Inferred implicit has an equivalent form but needs to be + manually simplified.\<close> by (transport eq: \<Omega>2.horiz_pathcomp_eq_horiz_pathcomp') refl also have ".. = \<beta> \<bullet> \<alpha>" by (rule pathcomp_eq_horiz_pathcomp') finally show "\<alpha> \<bullet> \<beta> = \<beta> \<bullet> \<alpha>" - by (this; reduce add: \<Omega>2_alt_def[symmetric]) - \<comment> \<open>TODO: The finishing call to `reduce` should be unnecessary with some - kind of definitional unfolding.\<close> + by this qed end diff --git a/hott/List+.thy b/hott/List+.thy index b73cc24..869d667 100644 --- a/hott/List+.thy +++ b/hott/List+.thy @@ -10,8 +10,8 @@ section \<open>Length\<close> definition [implicit]: "len \<equiv> ListRec ? Nat 0 (fn _ _ rec. suc rec)" experiment begin - Lemma "len [] \<equiv> ?n" by (subst comp) - Lemma "len [0, suc 0, suc (suc 0)] \<equiv> ?n" by (subst comp) + Lemma "len [] \<equiv> ?n" by (subst comp; typechk?) + Lemma "len [0, suc 0, suc (suc 0)] \<equiv> ?n" by (subst comp; typechk?)+ end |