From f46df86db9308dde29e0e5f97f54546ea1dc34bf Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Mon, 18 Jan 2021 23:49:13 +0000 Subject: Swapped notation for metas (now ?) and holes (now {}), other notation and name changes. --- hott/Identity.thy | 92 +++++++++++++++++++++++++++---------------------------- 1 file changed, 46 insertions(+), 46 deletions(-) (limited to 'hott/Identity.thy') diff --git a/hott/Identity.thy b/hott/Identity.thy index dc27ee8..0a31dc7 100644 --- a/hott/Identity.thy +++ b/hott/Identity.thy @@ -20,7 +20,7 @@ syntax "_Id" :: \o \ o \ o \ o\ translations "a =\<^bsub>A\<^esub> b" \ "CONST Id A a b" axiomatization where - \ \Here `A: U i` comes last because A is often implicit\ + \ \Here \A: U i\ comes last because A is often implicit\ IdF: "\a: A; b: A; A: U i\ \ a =\<^bsub>A\<^esub> b: U i" and IdI: "a: A \ refl a: a =\<^bsub>A\<^esub> a" and @@ -49,8 +49,8 @@ lemmas section \Path induction\ -\ \With `p: x = y` in the context the invokation `eq p` is essentially - `elim p x y`, with some extra bits before and after.\ +\ \With \p: x = y\ in the context the invokation \eq p\ is essentially + \elim p x y\, with some extra bits before and after.\ method_setup eq = \Args.term >> (fn tm => K (CONTEXT_METHOD ( @@ -109,13 +109,13 @@ method pathcomp for p q :: o = rule pathcomp[where ?p=p and ?q=q] section \Notation\ definition Id_i (infix "=" 110) - where [implicit]: "Id_i x y \ x =\<^bsub>?\<^esub> y" + where [implicit]: "Id_i x y \ x =\<^bsub>{}\<^esub> y" definition pathinv_i ("_\" [1000]) - where [implicit]: "pathinv_i p \ pathinv ? ? ? p" + where [implicit]: "pathinv_i p \ pathinv {} {} {} p" definition pathcomp_i (infixl "\" 121) - where [implicit]: "pathcomp_i p q \ pathcomp ? ? ? ? p q" + where [implicit]: "pathcomp_i p q \ pathcomp {} {} {} {} p q" translations "x = y" \ "x =\<^bsub>A\<^esub> y" @@ -125,7 +125,7 @@ translations section \Calculational reasoning\ -congruence "x = y" rhs y +calc "x = y" rhs y lemmas [sym] = pathinv[rotated 3] and @@ -144,8 +144,8 @@ Lemma (def) pathcomp_refl: shows "p \ (refl y) = p" by (eq p) (reduce, refl) -definition [implicit]: "lu p \ refl_pathcomp ? ? ? p" -definition [implicit]: "ru p \ pathcomp_refl ? ? ? p" +definition [implicit]: "lu p \ refl_pathcomp {} {} {} p" +definition [implicit]: "ru p \ pathcomp_refl {} {} {} p" translations "CONST lu p" \ "CONST refl_pathcomp A x y p" @@ -204,7 +204,7 @@ Lemma (def) ap: by (eq p) intro definition ap_i ("_[_]" [1000, 0]) - where [implicit]: "ap_i f p \ ap ? ? ? ? f p" + where [implicit]: "ap_i f p \ ap {} {} {} {} f p" translations "f[p]" \ "CONST ap A B x y f p" @@ -265,17 +265,17 @@ Lemma (def) transport: shows "P x \ P y" by (eq p) intro -definition transport_i ("trans") - where [implicit]: "trans P p \ transport ? P ? ? p" +definition transport_i ("transp") + where [implicit]: "transp P p \ transport {} P {} {} p" -translations "trans P p" \ "CONST transport A P x y p" +translations "transp P p" \ "CONST transport A P x y p" Lemma transport_comp [comp]: assumes "a: A" "A: U i" "\x. x: A \ P x: U i" - shows "trans P (refl a) \ id (P a)" + shows "transp P (refl a) \ id (P a)" unfolding transport_def by reduce Lemma apply_transport: @@ -284,7 +284,7 @@ Lemma apply_transport: "x: A" "y: A" "p: y =\<^bsub>A\<^esub> x" "u: P x" - shows "trans P p\ u: P y" + shows "transp P p\ u: P y" by typechk method transport uses eq = (rule apply_transport[OF _ _ _ _ eq]) @@ -304,7 +304,7 @@ Lemma (def) pathcomp_cancel_left: by (transport eq: pathcomp_assoc, transport eq: inv_pathcomp, transport eq: refl_pathcomp) refl - finally show "{}" by this + finally show "?" by this qed Lemma (def) pathcomp_cancel_right: @@ -323,7 +323,7 @@ Lemma (def) pathcomp_cancel_right: transport eq: pathcomp_assoc[symmetric], transport eq: pathcomp_inv, transport eq: pathcomp_refl) refl - finally show "{}" by this + finally show "?" by this qed method pathcomp_cancell = rule pathcomp_cancel_left[rotated 7] @@ -335,7 +335,7 @@ Lemma (def) transport_left_inv: "\x. x: A \ P x: U i" "x: A" "y: A" "p: x = y" - shows "(trans P p\) \ (trans P p) = id (P x)" + shows "(transp P p\) \ (transp P p) = id (P x)" by (eq p) (reduce, refl) Lemma (def) transport_right_inv: @@ -344,7 +344,7 @@ Lemma (def) transport_right_inv: "\x. x: A \ P x: U i" "x: A" "y: A" "p: x = y" - shows "(trans P p) \ (trans P p\) = id (P y)" + shows "(transp P p) \ (transp P p\) = id (P y)" by (eq p) (reduce, refl) Lemma (def) transport_pathcomp: @@ -354,11 +354,11 @@ Lemma (def) transport_pathcomp: "x: A" "y: A" "z: A" "u: P x" "p: x = y" "q: y = z" - shows "trans P q (trans P p u) = trans P (p \ q) u" + shows "transp P q (transp P p u) = transp P (p \ q) u" proof (eq p) fix x q u assuming "x: A" "q: x = z" "u: P x" - show "trans P q (trans P (refl x) u) = trans P ((refl x) \ q) u" + show "transp P q (transp P (refl x) u) = transp P ((refl x) \ q) u" by (eq q) (reduce, refl) qed @@ -370,7 +370,7 @@ Lemma (def) transport_compose_typefam: "x: A" "y: A" "p: x = y" "u: P (f x)" - shows "trans (fn x. P (f x)) p u = trans P f[p] u" + shows "transp (fn x. P (f x)) p u = transp P f[p] u" by (eq p) (reduce, refl) Lemma (def) transport_function_family: @@ -382,7 +382,7 @@ Lemma (def) transport_function_family: "x: A" "y: A" "u: P x" "p: x = y" - shows "trans Q p ((f x) u) = (f y) (trans P p u)" + shows "transp Q p ((f x) u) = (f y) (transp P p u)" by (eq p) (reduce, refl) Lemma (def) transport_const: @@ -390,19 +390,19 @@ Lemma (def) transport_const: "A: U i" "B: U i" "x: A" "y: A" "p: x = y" - shows "\b: B. trans (fn _. B) p b = b" + shows "\b: B. transp (fn _. B) p b = b" by intro (eq p, reduce, refl) -definition transport_const_i ("trans'_const") - where [implicit]: "trans_const B p \ transport_const ? B ? ? p" +definition transport_const_i ("transp'_c") + where [implicit]: "transp_c B p \ transport_const {} B {} {} p" -translations "trans_const B p" \ "CONST transport_const A B x y p" +translations "transp_c B p" \ "CONST transport_const A B x y p" Lemma transport_const_comp [comp]: assumes "x: A" "b: B" "A: U i" "B: U i" - shows "trans_const B (refl x) b \ refl b" + shows "transp_c B (refl x) b \ refl b" unfolding transport_const_def by reduce Lemma (def) pathlift: @@ -412,11 +412,11 @@ Lemma (def) pathlift: "x: A" "y: A" "p: x = y" "u: P x" - shows " = " + shows " = " by (eq p) (reduce, refl) definition pathlift_i ("lift") - where [implicit]: "lift P p u \ pathlift ? P ? ? p u" + where [implicit]: "lift P p u \ pathlift {} P {} {} p u" translations "lift P p u" \ "CONST pathlift A P x y p u" @@ -449,11 +449,11 @@ Lemma (def) apd: "f: \x: A. P x" "x: A" "y: A" "p: x = y" - shows "trans P p (f x) = f y" + shows "transp P p (f x) = f y" by (eq p) (reduce, refl) definition apd_i ("apd") - where [implicit]: "apd f p \ Identity.apd ? ? f ? ? p" + where [implicit]: "apd f p \ Identity.apd {} {} f {} {} p" translations "apd f p" \ "CONST Identity.apd A P f x y p" @@ -472,7 +472,7 @@ Lemma (def) apd_ap: "f: A \ B" "x: A" "y: A" "p: x = y" - shows "apd f p = trans_const B p (f x) \ f[p]" + shows "apd f p = transp_c B p (f x) \ f[p]" by (eq p) (reduce, refl) @@ -488,7 +488,7 @@ Lemma (def) right_whisker: have "s \ refl x = s" by (rule pathcomp_refl) also have ".. = t" by fact also have ".. = t \ refl x" by (rule pathcomp_refl[symmetric]) - finally show "{}" by this + finally show "?" by this qed done @@ -502,15 +502,15 @@ Lemma (def) left_whisker: have "refl x \ s = s" by (rule refl_pathcomp) also have ".. = t" by fact also have ".. = refl x \ t" by (rule refl_pathcomp[symmetric]) - finally show "{}" by this + finally show "?" by this qed done definition right_whisker_i (infix "\\<^sub>r" 121) - where [implicit]: "\ \\<^sub>r r \ right_whisker ? ? ? ? ? ? r \" + where [implicit]: "\ \\<^sub>r r \ right_whisker {} {} {} {} {} {} r \" definition left_whisker_i (infix "\\<^sub>l" 121) - where [implicit]: "r \\<^sub>l \ \ left_whisker ? ? ? ? ? ? r \" + where [implicit]: "r \\<^sub>l \ \ left_whisker {} {} {} {} {} {} r \" translations "\ \\<^sub>r r" \ "CONST right_whisker A a b c p q r \" @@ -532,8 +532,8 @@ method right_whisker = (rule right_whisker) section \Horizontal path-composition\ -text \Conditions under which horizontal path-composition is defined.\ locale horiz_pathcomposable = +\ \Conditions under which horizontal path-composition is defined.\ fixes i A a b c p q r s assumes [type]: @@ -615,17 +615,17 @@ Lemma (def) pathcomp_eq_horiz_pathcomp: have "refl (refl a) \ \ \ refl (refl a) = refl (refl a) \ \" by (rule pathcomp_refl) also have ".. = \" by (rule refl_pathcomp) - finally have eq\: "{} = \" by this + finally have eq\: "? = \" by this have "refl (refl a) \ \ \ refl (refl a) = refl (refl a) \ \" by (rule pathcomp_refl) also have ".. = \" by (rule refl_pathcomp) - finally have eq\: "{} = \" by this + finally have eq\: "? = \" by this have "refl (refl a) \ \ \ refl (refl a) \ (refl (refl a) \ \ \ refl (refl a)) - = \ \ {}" by right_whisker (fact eq\) + = \ \ ?" by right_whisker (fact eq\) also have ".. = \ \ \" by left_whisker (fact eq\) - finally show "{} = \ \ \" by this + finally show "? = \ \ \" by this qed Lemma (def) pathcomp_eq_horiz_pathcomp': @@ -637,17 +637,17 @@ Lemma (def) pathcomp_eq_horiz_pathcomp': have "refl (refl a) \ \ \ refl (refl a) = refl (refl a) \ \" by (rule pathcomp_refl) also have ".. = \" by (rule refl_pathcomp) - finally have eq\: "{} = \" by this + finally have eq\: "? = \" by this have "refl (refl a) \ \ \ refl (refl a) = refl (refl a) \ \" by (rule pathcomp_refl) also have ".. = \" by (rule refl_pathcomp) - finally have eq\: "{} = \" by this + finally have eq\: "? = \" by this have "refl (refl a) \ \ \ refl (refl a) \ (refl (refl a) \ \ \ refl (refl a)) - = \ \ {}" by right_whisker (fact eq\) + = \ \ ?" by right_whisker (fact eq\) also have ".. = \ \ \" by left_whisker (fact eq\) - finally show "{} = \ \ \" by this + finally show "? = \ \ \" by this qed Lemma (def) eckmann_hilton: -- cgit v1.2.3