From d19ac110d976581b595acfa3b4bb573790a92e84 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Thu, 30 Aug 2018 02:47:05 +0200 Subject: Some higher groupoid structure proofs --- EqualProps.thy | 56 +++++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 55 insertions(+), 1 deletion(-) (limited to 'EqualProps.thy') diff --git a/EqualProps.thy b/EqualProps.thy index a1d4c45..c114d37 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -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; @@ -205,10 +205,12 @@ axiomatization pathcomp :: "[Term, Term] \ Term" (infixl "\ 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" + 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 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) @@ -218,4 +220,56 @@ lemmas EqualProps_type [intro] = inv_type pathcomp_type lemmas EqualProps_comp [comp] = inv_comp pathcomp_comp +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) + + +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)+ +apply (subst pathcomp_comp) + + + end -- cgit v1.2.3 From 9b17aac85aa650a7a9d6463d3d01f1eb228d4572 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 11 Sep 2018 08:59:16 +0200 Subject: Go back to higher-order application notation --- EqualProps.thy | 85 +++++++++++++++++++++++++++++----------------------------- 1 file changed, 43 insertions(+), 42 deletions(-) (limited to 'EqualProps.thy') diff --git a/EqualProps.thy b/EqualProps.thy index c114d37..708eb33 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -14,7 +14,7 @@ begin section \Symmetry / Path inverse\ -definition inv :: "Term \ Term" ("_\" [1000] 1000) where "p\ \ ind\<^sub>= (\x. refl(x)) p" +definition inv :: "Term \ Term" ("_\" [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. @@ -22,7 +22,7 @@ text " " 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" + 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.\ @@ -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" .. @@ -46,14 +46,14 @@ 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 :: Term where "rpathcomp \ \<^bold>\_ _ p. ind\<^sub>= (\_. \<^bold>\_ q. ind\<^sub>= (\x. refl(x)) q) p" +definition rpathcomp :: Term 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)" + 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 @@ -81,7 +81,7 @@ proof qed fact corollary - assumes "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" + 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) @@ -90,11 +90,11 @@ text " " lemma rpathcomp_comp: - assumes "A: U(i)" and "a: A" - shows "rpathcomp`a`a`refl(a)`a`refl(a) \ refl(a)" + 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" + 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" @@ -114,11 +114,11 @@ proof compute qed (rule assms) qed (routine lems: assms 1 2 3) qed (routine lems: assms 1 2) - qed (rule assms) } + qed (rule assms) - show "(\<^bold>\y p. ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= refl q) p)`a`refl(a)`a`refl(a) \ refl(a)" + 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" + 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" @@ -135,11 +135,11 @@ proof compute qed (routine lems: assms 3 4) qed fact qed (routine lems: assms 1 2) - qed (routine lems: assms 1) } + qed (routine lems: assms 1) - show "(\<^bold>\p. ind\<^sub>= (\_. \<^bold>\z. \<^bold>\q. ind\<^sub>= refl q) p)`refl(a)`a`refl(a) \ refl(a)" + 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" + 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" @@ -152,11 +152,11 @@ proof compute 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) } + qed (routine lems: assms 1) - show "(ind\<^sub>=(\_. \<^bold>\z q. ind\<^sub>= refl q)(refl(a)))`a`refl(a) \ refl(a)" + 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" + 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" @@ -165,22 +165,22 @@ proof compute 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 } + qed fact - show "(\<^bold>\z q. ind\<^sub>= refl q)`a`refl(a) \ refl(a)" + next show "(\<^bold>\z q. ind\<^sub>= refl q)`a`(refl a) \ refl a" proof compute - { fix a assume 1: "a: A" + 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) } + qed (routine lems: assms 1) - show "(\<^bold>\q. ind\<^sub>= refl q)`refl(a) \ refl(a)" + 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)" + show "ind\<^sub>= refl (refl a) \ refl a" proof compute show "\x. x: A \ refl(x): x =\<^sub>A x" .. qed (routine lems: assms) @@ -196,23 +196,23 @@ text "The raw object lambda term is cumbersome to use, so we define a simpler co axiomatization pathcomp :: "[Term, Term] \ Term" (infixl "\" 120) where pathcomp_def: "\ - A: U(i); + 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" lemma pathcomp_type: - assumes "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" + 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" 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+ + 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 pathcomp_comp: - assumes "A : U(i)" and "a : A" shows "refl(a) \ refl(a) \ refl(a)" + assumes "A : U i" and "a : A" shows "(refl a) \ (refl a) \ refl a" by (subst pathcomp_def) (routine lems: assms rpathcomp_comp) @@ -223,44 +223,45 @@ lemmas EqualProps_comp [comp] = inv_comp pathcomp_comp section \Higher groupoid structure of types\ lemma - assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" + 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" + "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)" + 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" + 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" + 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)" + "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)" + 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)" + 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" + 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)" + "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 @@ -268,8 +269,8 @@ schematic_goal apply (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) apply (rule assms)+ -apply (subst pathcomp_comp) - +\ \Continue by substituting \refl x \ q = q\ etc.\ +sorry end -- cgit v1.2.3 From 637ee546f3eb9a927d83bd19ae0bee09031bd7d5 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 11 Sep 2018 10:20:26 +0200 Subject: Implementing univalence --- EqualProps.thy | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'EqualProps.thy') diff --git a/EqualProps.thy b/EqualProps.thy index 708eb33..f00020f 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -273,4 +273,9 @@ apply (rule assms)+ sorry +section \Transport\ + + + + end -- cgit v1.2.3 From cd7609be19289fefe5404fce6a3fed4957ae7157 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 11 Sep 2018 15:40:37 +0200 Subject: Running into trouble with the polymorphic identity function --- EqualProps.thy | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'EqualProps.thy') diff --git a/EqualProps.thy b/EqualProps.thy index f00020f..0107e8e 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -275,7 +275,22 @@ sorry section \Transport\ +definition transport :: "Term \ Term" where + "transport p \ ind\<^sub>= (\x. (\<^bold>\x. x)) p" +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) end -- cgit v1.2.3 From d7b9fc814d0fcb296156143a5d9bc3f5d9ad9ad1 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 11 Sep 2018 19:23:21 +0200 Subject: Add the univalence axiom --- EqualProps.thy | 2 ++ 1 file changed, 2 insertions(+) (limited to 'EqualProps.thy') diff --git a/EqualProps.thy b/EqualProps.thy index 0107e8e..4cfe280 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -292,5 +292,7 @@ lemma transport_comp: shows "transport (refl x) \ id" unfolding transport_def by (derive lems: assms) +text "Note that in our formulation, \transport\ is a polymorphic function!" + end -- cgit v1.2.3 From a1afde729f1d9b2f930696b117cfaec827eaa178 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Wed, 12 Sep 2018 06:33:55 +0200 Subject: Some final touchups before release 0.1 for the MS thesis --- EqualProps.thy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'EqualProps.thy') diff --git a/EqualProps.thy b/EqualProps.thy index 4cfe280..5db8487 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -278,6 +278,8 @@ section \Transport\ definition transport :: "Term \ Term" where "transport p \ ind\<^sub>= (\x. (\<^bold>\x. x)) p" +text "Note that \transport\ is a polymorphic function in our formulation." + lemma transport_type: assumes "A: U i" "P: A \ U i" @@ -292,7 +294,5 @@ lemma transport_comp: shows "transport (refl x) \ id" unfolding transport_def by (derive lems: assms) -text "Note that in our formulation, \transport\ is a polymorphic function!" - end -- cgit v1.2.3