From 24a0d9c9f72b54151f87332334f8ac488658351c Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Wed, 19 Sep 2018 15:07:05 +0200 Subject: Renaming --- EqualProps.thy | 177 --------------------------------------------------------- 1 file changed, 177 deletions(-) delete mode 100644 EqualProps.thy (limited to 'EqualProps.thy') diff --git a/EqualProps.thy b/EqualProps.thy deleted file mode 100644 index 847d964..0000000 --- a/EqualProps.thy +++ /dev/null @@ -1,177 +0,0 @@ -(* -Title: EqualProps.thy -Author: Joshua Chen -Date: 2018 - -Properties of equality -*) - -theory EqualProps -imports HoTT_Methods Equal Prod - -begin - - -section \Symmetry of equality/Path inverse\ - -definition inv :: "t \ t" ("_\" [1000] 1000) where "p\ \ ind\<^sub>= (\x. refl x) p" - -lemma inv_type: "\A: U i; x: A; y: A; p: x =\<^sub>A y\ \ p\: y =\<^sub>A x" -unfolding inv_def by (elim Equal_elim) routine - -lemma inv_comp: "\A: U i; a: A\ \ (refl a)\ \ refl a" -unfolding inv_def by compute routine - -declare - inv_type [intro] - inv_comp [comp] - - -section \Transitivity of equality/Path composition\ - -text \ -Composition function, of type @{term "x =\<^sub>A y \ (y =\<^sub>A z) \ (x =\<^sub>A z)"} polymorphic over @{term A}, @{term x}, @{term y}, and @{term z}. -\ - -definition pathcomp :: t where "pathcomp \ \<^bold>\p. ind\<^sub>= (\_. \<^bold>\q. ind\<^sub>= (\x. (refl x)) q) p" - -syntax "_pathcomp" :: "[t, t] \ t" (infixl "\" 120) -translations "p \ q" \ "CONST pathcomp`p`q" - -lemma pathcomp_type: - assumes "A: U i" "x: A" "y: A" "z: A" - shows "pathcomp: x =\<^sub>A y \ (y =\<^sub>A z) \ (x =\<^sub>A z)" -unfolding pathcomp_def by rule (elim Equal_elim, routine add: assms) - -corollary pathcomp_trans: - assumes "A: U i" and "x: A" "y: A" "z: A" and "p: x =\<^sub>A y" "q: y =\<^sub>A z" - shows "p \ q: x =\<^sub>A z" -by (routine add: assms pathcomp_type) - -lemma pathcomp_comp: - assumes "A: U i" and "a: A" - shows "(refl a) \ (refl a) \ refl a" -unfolding pathcomp_def proof compute - show "(ind\<^sub>= (\_. \<^bold>\q. ind\<^sub>= (\x. refl x) q) (refl a))`(refl a) \ refl a" - proof compute - show "\<^bold>\q. (ind\<^sub>= (\x. refl x) q): a =\<^sub>A a \ a =\<^sub>A a" - by (routine add: assms) - - show "(\<^bold>\q. (ind\<^sub>= (\x. refl x) q))`(refl a) \ refl a" - proof compute - show "\q. q: a =\<^sub>A a \ ind\<^sub>= (\x. refl x) q: a =\<^sub>A a" by (routine add: assms) - qed (derive lems: assms) - qed (routine add: assms) - - show "\p. p: a =\<^sub>A a \ ind\<^sub>= (\_. \<^bold>\q. ind\<^sub>= (\x. refl x) q) p: a =\<^sub>A a \ a =\<^sub>A a" - by (routine add: assms) -qed (routine add: assms) - -declare - pathcomp_type [intro] - pathcomp_trans [intro] - pathcomp_comp [comp] - - -section \Higher groupoid structure of types\ - -schematic_goal pathcomp_right_id: - assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" - shows "?a: p \ (refl y) =[x =\<^sub>A y] p" -proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) \ \@{method elim} does not seem to work with schematic goals.\ - show "\x. x: A \ refl(refl x): (refl x) \ (refl x) =[x =\<^sub>A x] (refl x)" - by (derive lems: assms) -qed (routine add: assms) - -schematic_goal pathcomp_left_id: - assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" - shows "?a: (refl x) \ p =[x =\<^sub>A y] p" -proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) - show "\x. x: A \ refl(refl x): (refl x) \ (refl x) =[x =\<^sub>A x] (refl x)" - by (derive lems: assms) -qed (routine add: assms) - -schematic_goal pathcomp_left_inv: - assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" - shows "?a: (p\ \ p) =[y =\<^sub>A y] refl(y)" -proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) - show "\x. x: A \ refl(refl x): (refl x)\ \ (refl x) =[x =\<^sub>A x] (refl x)" - by (derive lems: assms) -qed (routine add: assms) - -schematic_goal pathcomp_right_inv: - assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" - shows "?a: (p \ p\) =[x =\<^sub>A x] refl(x)" -proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) - show "\x. x: A \ refl(refl x): (refl x) \ (refl x)\ =[x =\<^sub>A x] (refl x)" - by (derive lems: assms) -qed (routine add: assms) - -schematic_goal inv_involutive: - assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" - shows "?a: p\\ =[x =\<^sub>A y] p" -proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) - show "\x. x: A \ refl(refl x): (refl x)\\ =[x =\<^sub>A x] (refl x)" - by (derive lems: assms) -qed (routine add: assms) - -text \All of the propositions above have the same proof term, which we abbreviate here.\ -abbreviation \ :: "t \ t" where "\ p \ ind\<^sub>= (\x. refl (refl x)) p" - -text \The next proof has a triply-nested path induction.\ - -lemma pathcomp_assoc: - assumes "A: U i" "x: A" "y: A" "z: A" "w: A" - shows "\<^bold>\p. ind\<^sub>= (\_. \<^bold>\q. ind\<^sub>= (\_. \<^bold>\r. \ r) q) p: - \p: x =\<^sub>A y. \q: y =\<^sub>A z. \r: z =\<^sub>A w. p \ (q \ r) =[x =\<^sub>A w] (p \ q) \ r" -proof - show "\p. p: x =\<^sub>A y \ ind\<^sub>= (\_. \<^bold>\q. ind\<^sub>= (\_. \<^bold>\r. \ r) q) p: - \q: y =\<^sub>A z. \r: z =\<^sub>A w. p \ (q \ r) =[x =\<^sub>A w] p \ q \ r" - proof (elim Equal_elim) - fix x assume 1: "x: A" - show "\<^bold>\q. ind\<^sub>= (\_. \<^bold>\r. \ r) q: - \q: x =\<^sub>A z. \r: z =\<^sub>A w. refl x \ (q \ r) =[x =\<^sub>A w] refl x \ q \ r" - proof - show "\q. q: x =\<^sub>A z \ ind\<^sub>= (\_. \<^bold>\r. \ r) q: - \r: z =\<^sub>A w. refl x \ (q \ r) =[x =\<^sub>A w] refl x \ q \ r" - proof (elim Equal_elim) - fix x assume *: "x: A" - show "\<^bold>\r. \ r: \r: x =\<^sub>A w. refl x \ (refl x \ r) =[x =\<^sub>A w] refl x \ refl x \ r" - proof - show "\r. r: x =[A] w \ \ r: refl x \ (refl x \ r) =[x =[A] w] refl x \ refl x \ r" - by (elim Equal_elim, derive lems: * assms) - qed (routine add: * assms) - qed (routine add: 1 assms) - qed (routine add: 1 assms) - - text \ - In the following part @{method derive} fails to obtain the correct subgoals, so we have to prove the statement manually. - \ - fix y p assume 2: "y: A" "p: x =\<^sub>A y" - show "\q: y =\<^sub>A z. \r: z =\<^sub>A w. p \ (q \ r) =[x =\<^sub>A w] p \ q \ r: U i" - proof (routine add: assms) - fix q assume 3: "q: y =\<^sub>A z" - show "\r: z =\<^sub>A w. p \ (q \ r) =[x =\<^sub>A w] p \ q \ r: U i" - proof (routine add: assms) - show "\r. r: z =[A] w \ p \ (q \ r): x =[A] w" and "\r. r: z =[A] w \ p \ q \ r: x =[A] w" - by (routine add: 1 2 3 assms) - qed (routine add: 1 assms) - qed fact+ - qed fact+ -qed (routine add: assms) - - -section \Transport\ - -definition transport :: "t \ t" where "transport p \ ind\<^sub>= (\_. (\<^bold>\x. x)) p" - -text \Note that @{term transport} is a polymorphic function in our formulation.\ - -lemma transport_type: "\p: x =\<^sub>A y; x: A; y: A; A: U i; P: A \ U i\ \ transport p: P x \ P y" -unfolding transport_def by (elim Equal_elim) routine - -lemma transport_comp: "\A: U i; x: A\ \ transport (refl x) \ id" -unfolding transport_def by derive - - -end -- cgit v1.2.3