From 746fab6476dc622a982d5ebaeb30a2e1426c3316 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Sun, 19 Aug 2018 17:28:48 +0200 Subject: Higher groupoid structure of types --- EqualProps.thy | 71 ++++++++++++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 67 insertions(+), 4 deletions(-) (limited to 'EqualProps.thy') diff --git a/EqualProps.thy b/EqualProps.thy index a1d4c45..be8e53e 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -33,7 +33,7 @@ text " " lemma inv_comp: - assumes "A : U(i)" and "a : A" shows "(refl a)\ \ refl(a)" + assumes "A : U(i)" and "a : A" shows "(refl(a))\ \ refl(a)" unfolding inv_def proof compute show "\x. x: A \ refl x: x =\<^sub>A x" .. @@ -194,7 +194,7 @@ qed fact text "The raw object lambda term is cumbersome to use, so we define a simpler constant instead." -axiomatization pathcomp :: "[Term, Term] \ Term" (infixl "\" 60) where +axiomatization pathcomp :: "[Term, Term] \ Term" (infixl "\" 120) where pathcomp_def: "\ A: U(i); x: A; y: A; z: A; @@ -214,8 +214,71 @@ lemma pathcomp_comp: by (subst pathcomp_def) (routine lems: assms rpathcomp_comp) -lemmas EqualProps_type [intro] = inv_type pathcomp_type -lemmas EqualProps_comp [comp] = inv_comp pathcomp_comp +lemmas inv_type [intro] +lemmas pathcomp_type [intro] +lemmas inv_comp [comp] +lemmas pathcomp_comp [comp] + + +section \Weak higher groupoid structure of types\ + +schematic_goal whg1a: + assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" + shows "?a: p =[x =\<^sub>A y] (p \ (refl(y)))" +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) \ refl(x))" + by compute (routine lems: assms) +qed (routine lems: assms) + +schematic_goal whg1b: + assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" + shows "?a: p =[x =\<^sub>A y] (refl(x) \ 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) \ refl(x))" + by compute (routine lems: assms) +qed (routine lems: assms) + +schematic_goal whg2a: + 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 (compute | routine lems: assms)+ +qed (routine lems: assms)+ + +schematic_goal whg2b: + 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 (compute | routine lems: assms)+ +qed (routine lems: assms)+ + +schematic_goal whg3: + 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 (compute | routine lems: assms)+ +qed (routine lems: assms) + + +lemma assumes "A: U(i)" shows "\x. x: A \ refl(x): x =\<^sub>A x" +by (rule Prod_atomize[where ?A=A and ?B="\x. x =\<^sub>A x"]) (routine lems: assms) + + +schematic_goal + assumes + "A: U(i)" and + "x: A" "y: A" "z: A" "w: A" and + "p: x =\<^sub>A y" "q: y =\<^sub>A z" "r: z =\<^sub>A w" + shows + "?a: p \ (q \ r) =[x =\<^sub>A w] (p \ q) \ r" +proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) + fix y assume "y: A" + show "refl(q \ r): refl(y) \ (q \ r) =[y =\<^sub>A w] (refl(y) \ q) \ r" + proof (compute lems: whg1b) + end -- cgit v1.2.3 From dcf87145a1059659099bbecde55973de0d36d43f Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 18 Sep 2018 03:04:37 +0200 Subject: Theories fully reorganized. Well-formedness rules removed. New methods etc. --- EqualProps.thy | 398 +++++++++++++-------------------------------------------- 1 file changed, 87 insertions(+), 311 deletions(-) (limited to 'EqualProps.thy') diff --git a/EqualProps.thy b/EqualProps.thy index 19c788c..abb2623 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -1,361 +1,137 @@ -(* Title: HoTT/EqualProps.thy - Author: Josh Chen +(* +Title: EqualProps.thy +Author: Joshua Chen +Date: 2018 Properties of equality *) theory EqualProps - imports - HoTT_Methods - Equal - Prod +imports HoTT_Methods Equal Prod + begin -section \Symmetry / Path inverse\ - -definition inv :: "t \ t" ("_\" [1000] 1000) where "p\ \ ind\<^sub>= (\x. (refl x)) p" - -text " - In the proof below we begin by using path induction on \p\ with the application of \rule Equal_elim\, telling Isabelle the specific substitutions to use. - The proof is finished with a standard application of the relevant type rules. -" - -lemma inv_type: - assumes "A : U i" and "x : A" and "y : A" and "p: x =\<^sub>A y" shows "p\: y =\<^sub>A x" -unfolding inv_def -by (rule Equal_elim[where ?x=x and ?y=y]) (routine lems: assms) - \ \The type doesn't depend on \p\ so we don't need to specify \?p\ in the \where\ clause above.\ - -text " - The next proof requires explicitly telling Isabelle what to substitute on the RHS of the typing judgment after the initial application of the type rules. - (If viewing this inside Isabelle, place the cursor after the \proof\ statement and observe the second subgoal.) -" - -lemma inv_comp: - assumes "A : U i " and "a : A" shows "(refl a)\ \ refl a" -unfolding inv_def -proof compute - show "\x. x: A \ refl x: x =\<^sub>A x" .. -qed (routine lems: assms) - - -section \Transitivity / Path composition\ - -text " - Raw composition function, of type \\x:A. \y:A. x =\<^sub>A y \ (\z:A. y =\<^sub>A z \ x =\<^sub>A z)\ polymorphic over the type \A\. -" - -definition rpathcomp :: t where "rpathcomp \ \<^bold>\_ _ p. ind\<^sub>= (\_. \<^bold>\_ q. ind\<^sub>= (\x. (refl x)) q) p" - -text " - More complicated proofs---the nested path inductions require more explicit step-by-step rule applications: -" - -lemma rpathcomp_type: - assumes "A: U i" - shows "rpathcomp: \x:A. \y:A. x =\<^sub>A y \ (\z:A. y =\<^sub>A z \ x =\<^sub>A z)" -unfolding rpathcomp_def -proof - fix x assume 1: "x: A" - show "\<^bold>\y p. ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= refl q) p: \y:A. x =\<^sub>A y \ (\z:A. y =\<^sub>A z \ x =\<^sub>A z)" - proof - fix y assume 2: "y: A" - show "\<^bold>\p. ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= refl q) p: x =\<^sub>A y \ (\z:A. y =\<^sub>A z \ x =\<^sub>A z)" - proof - fix p assume 3: "p: x =\<^sub>A y" - show "ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= refl q) p: \z:A. y =\<^sub>A z \ x =\<^sub>A z" - proof (rule Equal_elim[where ?x=x and ?y=y]) - show "\u. u: A \ \<^bold>\z q. ind\<^sub>= refl q: \z:A. u =\<^sub>A z \ u =\<^sub>A z" - proof - show "\u z. \u: A; z: A\ \ \<^bold>\q. ind\<^sub>= refl q: u =\<^sub>A z \ u =\<^sub>A z" - proof - fix u z q assume asm: "u: A" "z: A" "q: u =\<^sub>A z" - show "ind\<^sub>= refl q: u =\<^sub>A z" - by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms asm) - qed (routine lems: assms) - qed (rule assms) - qed (routine lems: assms 1 2 3) - qed (routine lems: assms 1 2) - qed (rule assms) -qed fact - -corollary - assumes "A: U i" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" - shows "rpathcomp`x`y`p`z`q: x =\<^sub>A z" - by (routine lems: assms rpathcomp_type) - -text " - The following proof is very long, chiefly because for every application of \`\ we have to show the wellformedness of the type family appearing in the equality computation rule. -" - -lemma rpathcomp_comp: - assumes "A: U i" and "a: A" - shows "rpathcomp`a`a`(refl a)`a`(refl a) \ refl a" -unfolding rpathcomp_def -proof compute - fix x assume 1: "x: A" - show "\<^bold>\y p. ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= refl q) p: \y:A. x =\<^sub>A y \ (\z:A. y =\<^sub>A z \ x =\<^sub>A z)" - proof - fix y assume 2: "y: A" - show "\<^bold>\p. ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= refl q) p: x =\<^sub>A y \ (\z:A. y =\<^sub>A z \ x =\<^sub>A z)" - proof - fix p assume 3: "p: x =\<^sub>A y" - show "ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= refl q) p: \z:A. y =\<^sub>A z \ x =\<^sub>A z" - proof (rule Equal_elim[where ?x=x and ?y=y]) - show "\u. u: A \ \<^bold>\z q. ind\<^sub>= refl q: \z:A. u =\<^sub>A z \ u =\<^sub>A z" - proof - show "\u z. \u: A; z: A\ \ \<^bold>\q. ind\<^sub>= refl q: u =\<^sub>A z \ u =\<^sub>A z" - proof - fix u z assume asm: "u: A" "z: A" - show "\q. q: u =\<^sub>A z \ ind\<^sub>= refl q: u =\<^sub>A z" - by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms asm) - qed (routine lems: assms) - qed (rule assms) - qed (routine lems: assms 1 2 3) - qed (routine lems: assms 1 2) - qed (rule assms) - - next show "(\<^bold>\y p. ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= refl q) p)`a`(refl a)`a`(refl a) \ refl a" - proof compute - fix y assume 1: "y: A" - show "\<^bold>\p. ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= refl q) p: a =\<^sub>A y \ (\z:A. y =\<^sub>A z \ a =\<^sub>A z)" - proof - fix p assume 2: "p: a =\<^sub>A y" - show "ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= refl q) p: \z:A. y =\<^sub>A z \ a =\<^sub>A z" - proof (rule Equal_elim[where ?x=a and ?y=y]) - fix u assume 3: "u: A" - show "\<^bold>\z q. ind\<^sub>= refl q: \z:A. u =\<^sub>A z \ u =\<^sub>A z" - proof - fix z assume 4: "z: A" - show "\<^bold>\q. ind\<^sub>= refl q: u =\<^sub>A z \ u =\<^sub>A z" - proof - show "\q. q: u =\<^sub>A z \ ind\<^sub>= refl q: u =\<^sub>A z" - by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms 3 4) - qed (routine lems: assms 3 4) - qed fact - qed (routine lems: assms 1 2) - qed (routine lems: assms 1) - - next show "(\<^bold>\p. ind\<^sub>= (\_. \<^bold>\z. \<^bold>\q. ind\<^sub>= refl q) p)`(refl a)`a`(refl a) \ refl a" - proof compute - fix p assume 1: "p: a =\<^sub>A a" - show "ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= refl q) p: \z:A. a =\<^sub>A z \ a =\<^sub>A z" - proof (rule Equal_elim[where ?x=a and ?y=a]) - fix u assume 2: "u: A" - show "\<^bold>\z q. ind\<^sub>= refl q: \z:A. u =\<^sub>A z \ u =\<^sub>A z" - proof - fix z assume 3: "z: A" - show "\<^bold>\q. ind\<^sub>= refl q: u =\<^sub>A z \ u =\<^sub>A z" - proof - show "\q. q: u =\<^sub>A z \ ind\<^sub>= refl q: u =\<^sub>A z" - by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms 2 3) - qed (routine lems: assms 2 3) - qed fact - qed (routine lems: assms 1) - - next show "(ind\<^sub>=(\_. \<^bold>\z q. ind\<^sub>= refl q)(refl a))`a`(refl a) \ refl a" - proof compute - fix u assume 1: "u: A" - show "\<^bold>\z q. ind\<^sub>= refl q: \z:A. u =\<^sub>A z \ u =\<^sub>A z" - proof - fix z assume 2: "z: A" - show "\<^bold>\q. ind\<^sub>= refl q: u =\<^sub>A z \ u =\<^sub>A z" - proof - show "\q. q: u =\<^sub>A z \ ind\<^sub>= refl q: u =\<^sub>A z" - by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms 1 2) - qed (routine lems: assms 1 2) - qed fact - - next show "(\<^bold>\z q. ind\<^sub>= refl q)`a`(refl a) \ refl a" - proof compute - fix a assume 1: "a: A" - show "\<^bold>\q. ind\<^sub>= refl q: a =\<^sub>A a \ a =\<^sub>A a" - proof - show "\q. q: a =\<^sub>A a \ ind\<^sub>= refl q: a =\<^sub>A a" - by (rule Equal_elim[where ?x=a and ?y=a]) (routine lems: assms 1) - qed (routine lems: assms 1) - - next show "(\<^bold>\q. ind\<^sub>= refl q)`(refl a) \ refl a" - proof compute - show "\p. p: a =\<^sub>A a \ ind\<^sub>= refl p: a =\<^sub>A a" - by (rule Equal_elim[where ?x=a and ?y=a]) (routine lems: assms) - show "ind\<^sub>= refl (refl a) \ refl a" - proof compute - show "\x. x: A \ refl(x): x =\<^sub>A x" .. - qed (routine lems: assms) - qed (routine lems: assms) - qed fact - qed (routine lems: assms) - qed (routine lems: assms) - qed fact -qed fact - - -text "The raw object lambda term is cumbersome to use, so we define a simpler constant instead." - -axiomatization pathcomp :: "[t, t] \ t" (infixl "\" 120) where - pathcomp_def: "\ - A: U i; - x: A; y: A; z: A; - p: x =\<^sub>A y; q: y =\<^sub>A z - \ \ p \ q \ rpathcomp`x`y`p`z`q" +section \Symmetry of equality/Path inverse\ +definition inv :: "t \ t" ("_\" [1000] 1000) where "p\ \ ind\<^sub>= (\x. refl x) p" -lemma pathcomp_type: - assumes "A: U i" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" - shows "p \ q: x =\<^sub>A z" +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 -proof (subst pathcomp_def) - show "A: U i" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" by fact+ -qed (routine lems: assms rpathcomp_type) +lemma inv_comp: "\A: U i; a: A\ \ (refl a)\ \ refl a" +unfolding inv_def by compute routine -lemma pathcomp_comp: - assumes "A : U i" and "a : A" shows "(refl a) \ (refl a) \ refl a" -by (subst pathcomp_def) (routine lems: assms rpathcomp_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}. +\ -lemmas inv_type [intro] -lemmas pathcomp_type [intro] +definition pathcomp :: t where "pathcomp \ \<^bold>\p. ind\<^sub>= (\_. \<^bold>\q. ind\<^sub>= (\x. (refl x)) q) p" -lemmas inv_comp [comp] -lemmas pathcomp_comp [comp] +syntax "_pathcomp" :: "[t, t] \ t" (infixl "\" 120) +translations "p \ q" \ "CONST pathcomp`p`q" +lemma pathcomp_type: + assumes "A: U i" and "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) -section \Weak higher groupoid structure of types\ +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) -schematic_goal whg1a: +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) + + +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 =[x =\<^sub>A y] (p \ (refl(y)))" -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) \ refl(x))" - by compute (routine lems: assms) -qed (routine lems: assms) + 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 pathcomp_comp) +qed (routine add: assms pathcomp_type) -schematic_goal whg1b: +schematic_goal pathcomp_left_id: assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" - shows "?a: p =[x =\<^sub>A y] (refl(x) \ p)" + 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) =[x =\<^sub>A x] (refl(x) \ refl(x))" - by compute (routine lems: assms) -qed (routine lems: assms) + show "\x. x: A \ refl(refl x): (refl x) \ (refl x) =[x =\<^sub>A x] (refl x)" + by (derive lems: assms pathcomp_comp) +qed (routine add: assms pathcomp_type) -schematic_goal whg2a: +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 (compute | routine lems: assms)+ -qed (routine lems: assms)+ + show "\x. x: A \ refl(refl x): (refl x)\ \ (refl x) =[x =\<^sub>A x] (refl x)" + by (derive lems: assms inv_comp pathcomp_comp) +qed (routine add: assms inv_type pathcomp_type) -schematic_goal whg2b: +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 (compute | routine lems: assms)+ -qed (routine lems: assms)+ + show "\x. x: A \ refl(refl x): (refl x) \ (refl x)\ =[x =\<^sub>A x] (refl x)" + by (derive lems: assms inv_comp pathcomp_comp) +qed (routine add: assms inv_type pathcomp_type) -schematic_goal whg3: +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 (compute | routine lems: assms)+ -qed (routine lems: assms) - - -lemma assumes "A: U(i)" shows "\x. x: A \ refl(x): x =\<^sub>A x" -by (rule Prod_atomize[where ?A=A and ?B="\x. x =\<^sub>A x"]) (routine lems: assms) - + show "\x. x: A \ refl(refl x): (refl x)\\ =[x =\<^sub>A x] (refl x)" + by (derive lems: assms inv_comp) +qed (routine add: assms inv_type) -schematic_goal +schematic_goal pathcomp_assoc: assumes - "A: U(i)" and - "x: A" "y: A" "z: A" "w: A" and + "A: U(i)" + "x: A" "y: A" "z: A" "w: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" "r: z =\<^sub>A w" shows "?a: p \ (q \ r) =[x =\<^sub>A w] (p \ q) \ r" proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) - fix y assume "y: A" - show "refl(q \ r): refl(y) \ (q \ r) =[y =\<^sub>A w] (refl(y) \ q) \ r" - proof (compute lems: whg1b) - - -section \Higher groupoid structure of types\ - -lemma - assumes "A: U i" "x: A" "y: A" "p: x =\<^sub>A y" - shows - "ind\<^sub>= (\u. refl (refl u)) p: p =[x =\<^sub>A y] p \ (refl y)" and - "ind\<^sub>= (\u. refl (refl u)) p: p =[x =\<^sub>A y] (refl x) \ p" - -proof - - show "ind\<^sub>= (\u. refl (refl u)) p: p =[x =[A] y] p \ (refl y)" - by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+ - - show "ind\<^sub>= (\u. refl (refl u)) p: p =[x =[A] y] (refl x) \ p" - by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+ -qed - - -lemma - assumes "A: U i" "x: A" "y: A" "p: x =\<^sub>A y" - shows - "ind\<^sub>= (\u. refl (refl u)) p: p\ \ p =[y =\<^sub>A y] (refl y)" and - "ind\<^sub>= (\u. refl (refl u)) p: p \ p\ =[x =\<^sub>A x] (refl x)" - -proof - - show "ind\<^sub>= (\u. refl (refl u)) p: p\ \ p =[y =\<^sub>A y] (refl y)" - by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+ - - show "ind\<^sub>= (\u. refl (refl u)) p: p \ p\ =[x =\<^sub>A x] (refl x)" - by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+ -qed - - -lemma - assumes "A: U i" "x: A" "y: A" "p: x =\<^sub>A y" - shows "ind\<^sub>= (\u. refl (refl u)) p: p\\ =[x =\<^sub>A y] p" -by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms) - -text "Next we construct a proof term of associativity of path composition." - -schematic_goal - assumes - "A: U i" - "x: A" "y: A" "z: A" "w: A" - "p: x =\<^sub>A y" "q: y =\<^sub>A z" "r: z =\<^sub>A w" - shows - "?a: p \ (q \ r) =[x =\<^sub>A z] (p \ q) \ r" - -apply (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) -apply (rule assms)+ -\ \Continue by substituting \refl x \ q = q\ etc.\ -sorry + fix x assume "x: A" + show "refl (q \ r): (refl x) \ (q \ r) =[x =\<^sub>A w] ((refl x) \ q) \ r" + \ \This requires substitution of *propositional* equality. \ + sorry + oops section \Transport\ -definition transport :: "t \ t" where - "transport p \ ind\<^sub>= (\x. (\<^bold>\x. x)) p" +definition transport :: "t \ t" where "transport p \ ind\<^sub>= (\_. (\<^bold>\x. x)) p" -text "Note that \transport\ is a polymorphic function in our formulation." +text \Note that @{term transport} is a polymorphic function in our formulation.\ -lemma transport_type: - assumes - "A: U i" "P: A \ U i" - "x: A" "y: A" - "p: x =\<^sub>A y" - shows "transport p: P x \ P y" -unfolding transport_def -by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (routine lems: assms) - -lemma transport_comp: - assumes "A: U i" and "x: A" - shows "transport (refl x) \ id" -unfolding transport_def by (derive lems: assms) +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