From 6402b72747c153798b5a9ef5175038e5c1409be5 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 21 Aug 2018 14:37:22 +0200 Subject: Create LICENSE.md --- LICENSE.md | 165 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 165 insertions(+) create mode 100644 LICENSE.md diff --git a/LICENSE.md b/LICENSE.md new file mode 100644 index 0000000..65c5ca8 --- /dev/null +++ b/LICENSE.md @@ -0,0 +1,165 @@ + GNU LESSER GENERAL PUBLIC LICENSE + Version 3, 29 June 2007 + + Copyright (C) 2007 Free Software Foundation, Inc. + Everyone is permitted to copy and distribute verbatim copies + of this license document, but changing it is not allowed. + + + This version of the GNU Lesser General Public License incorporates +the terms and conditions of version 3 of the GNU General Public +License, supplemented by the additional permissions listed below. + + 0. Additional Definitions. + + As used herein, "this License" refers to version 3 of the GNU Lesser +General Public License, and the "GNU GPL" refers to version 3 of the GNU +General Public License. + + "The Library" refers to a covered work governed by this License, +other than an Application or a Combined Work as defined below. + + An "Application" is any work that makes use of an interface provided +by the Library, but which is not otherwise based on the Library. +Defining a subclass of a class defined by the Library is deemed a mode +of using an interface provided by the Library. + + A "Combined Work" is a work produced by combining or linking an +Application with the Library. The particular version of the Library +with which the Combined Work was made is also called the "Linked +Version". + + The "Minimal Corresponding Source" for a Combined Work means the +Corresponding Source for the Combined Work, excluding any source code +for portions of the Combined Work that, considered in isolation, are +based on the Application, and not on the Linked Version. + + The "Corresponding Application Code" for a Combined Work means the +object code and/or source code for the Application, including any data +and utility programs needed for reproducing the Combined Work from the +Application, but excluding the System Libraries of the Combined Work. + + 1. Exception to Section 3 of the GNU GPL. + + You may convey a covered work under sections 3 and 4 of this License +without being bound by section 3 of the GNU GPL. + + 2. Conveying Modified Versions. + + If you modify a copy of the Library, and, in your modifications, a +facility refers to a function or data to be supplied by an Application +that uses the facility (other than as an argument passed when the +facility is invoked), then you may convey a copy of the modified +version: + + a) under this License, provided that you make a good faith effort to + ensure that, in the event an Application does not supply the + function or data, the facility still operates, and performs + whatever part of its purpose remains meaningful, or + + b) under the GNU GPL, with none of the additional permissions of + this License applicable to that copy. + + 3. Object Code Incorporating Material from Library Header Files. + + The object code form of an Application may incorporate material from +a header file that is part of the Library. You may convey such object +code under terms of your choice, provided that, if the incorporated +material is not limited to numerical parameters, data structure +layouts and accessors, or small macros, inline functions and templates +(ten or fewer lines in length), you do both of the following: + + a) Give prominent notice with each copy of the object code that the + Library is used in it and that the Library and its use are + covered by this License. + + b) Accompany the object code with a copy of the GNU GPL and this license + document. + + 4. Combined Works. + + You may convey a Combined Work under terms of your choice that, +taken together, effectively do not restrict modification of the +portions of the Library contained in the Combined Work and reverse +engineering for debugging such modifications, if you also do each of +the following: + + a) Give prominent notice with each copy of the Combined Work that + the Library is used in it and that the Library and its use are + covered by this License. + + b) Accompany the Combined Work with a copy of the GNU GPL and this license + document. + + c) For a Combined Work that displays copyright notices during + execution, include the copyright notice for the Library among + these notices, as well as a reference directing the user to the + copies of the GNU GPL and this license document. + + d) Do one of the following: + + 0) Convey the Minimal Corresponding Source under the terms of this + License, and the Corresponding Application Code in a form + suitable for, and under terms that permit, the user to + recombine or relink the Application with a modified version of + the Linked Version to produce a modified Combined Work, in the + manner specified by section 6 of the GNU GPL for conveying + Corresponding Source. + + 1) Use a suitable shared library mechanism for linking with the + Library. A suitable mechanism is one that (a) uses at run time + a copy of the Library already present on the user's computer + system, and (b) will operate properly with a modified version + of the Library that is interface-compatible with the Linked + Version. + + e) Provide Installation Information, but only if you would otherwise + be required to provide such information under section 6 of the + GNU GPL, and only to the extent that such information is + necessary to install and execute a modified version of the + Combined Work produced by recombining or relinking the + Application with a modified version of the Linked Version. (If + you use option 4d0, the Installation Information must accompany + the Minimal Corresponding Source and Corresponding Application + Code. If you use option 4d1, you must provide the Installation + Information in the manner specified by section 6 of the GNU GPL + for conveying Corresponding Source.) + + 5. Combined Libraries. + + You may place library facilities that are a work based on the +Library side by side in a single library together with other library +facilities that are not Applications and are not covered by this +License, and convey such a combined library under terms of your +choice, if you do both of the following: + + a) Accompany the combined library with a copy of the same work based + on the Library, uncombined with any other library facilities, + conveyed under the terms of this License. + + b) Give prominent notice with the combined library that part of it + is a work based on the Library, and explaining where to find the + accompanying uncombined form of the same work. + + 6. Revised Versions of the GNU Lesser General Public License. + + The Free Software Foundation may publish revised and/or new versions +of the GNU Lesser General Public License from time to time. Such new +versions will be similar in spirit to the present version, but may +differ in detail to address new problems or concerns. + + Each version is given a distinguishing version number. If the +Library as you received it specifies that a certain numbered version +of the GNU Lesser General Public License "or any later version" +applies to it, you have the option of following the terms and +conditions either of that published version or of any later version +published by the Free Software Foundation. If the Library as you +received it does not specify a version number of the GNU Lesser +General Public License, you may choose any version of the GNU Lesser +General Public License ever published by the Free Software Foundation. + + If the Library as you received it specifies that a proxy can decide +whether future versions of the GNU Lesser General Public License shall +apply, that proxy's public statement of acceptance of any version is +permanent authorization for you to choose that version for the +Library. -- cgit v1.2.3 From 5193d4dd1ebef7fa000489710ff138ab98876c52 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 21 Aug 2018 14:38:28 +0200 Subject: Rename LICENSE.md to LICENSE --- LICENSE | 165 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ LICENSE.md | 165 ------------------------------------------------------------- 2 files changed, 165 insertions(+), 165 deletions(-) create mode 100644 LICENSE delete mode 100644 LICENSE.md diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..65c5ca8 --- /dev/null +++ b/LICENSE @@ -0,0 +1,165 @@ + GNU LESSER GENERAL PUBLIC LICENSE + Version 3, 29 June 2007 + + Copyright (C) 2007 Free Software Foundation, Inc. + Everyone is permitted to copy and distribute verbatim copies + of this license document, but changing it is not allowed. + + + This version of the GNU Lesser General Public License incorporates +the terms and conditions of version 3 of the GNU General Public +License, supplemented by the additional permissions listed below. + + 0. Additional Definitions. + + As used herein, "this License" refers to version 3 of the GNU Lesser +General Public License, and the "GNU GPL" refers to version 3 of the GNU +General Public License. + + "The Library" refers to a covered work governed by this License, +other than an Application or a Combined Work as defined below. + + An "Application" is any work that makes use of an interface provided +by the Library, but which is not otherwise based on the Library. +Defining a subclass of a class defined by the Library is deemed a mode +of using an interface provided by the Library. + + A "Combined Work" is a work produced by combining or linking an +Application with the Library. The particular version of the Library +with which the Combined Work was made is also called the "Linked +Version". + + The "Minimal Corresponding Source" for a Combined Work means the +Corresponding Source for the Combined Work, excluding any source code +for portions of the Combined Work that, considered in isolation, are +based on the Application, and not on the Linked Version. + + The "Corresponding Application Code" for a Combined Work means the +object code and/or source code for the Application, including any data +and utility programs needed for reproducing the Combined Work from the +Application, but excluding the System Libraries of the Combined Work. + + 1. Exception to Section 3 of the GNU GPL. + + You may convey a covered work under sections 3 and 4 of this License +without being bound by section 3 of the GNU GPL. + + 2. Conveying Modified Versions. + + If you modify a copy of the Library, and, in your modifications, a +facility refers to a function or data to be supplied by an Application +that uses the facility (other than as an argument passed when the +facility is invoked), then you may convey a copy of the modified +version: + + a) under this License, provided that you make a good faith effort to + ensure that, in the event an Application does not supply the + function or data, the facility still operates, and performs + whatever part of its purpose remains meaningful, or + + b) under the GNU GPL, with none of the additional permissions of + this License applicable to that copy. + + 3. Object Code Incorporating Material from Library Header Files. + + The object code form of an Application may incorporate material from +a header file that is part of the Library. You may convey such object +code under terms of your choice, provided that, if the incorporated +material is not limited to numerical parameters, data structure +layouts and accessors, or small macros, inline functions and templates +(ten or fewer lines in length), you do both of the following: + + a) Give prominent notice with each copy of the object code that the + Library is used in it and that the Library and its use are + covered by this License. + + b) Accompany the object code with a copy of the GNU GPL and this license + document. + + 4. Combined Works. + + You may convey a Combined Work under terms of your choice that, +taken together, effectively do not restrict modification of the +portions of the Library contained in the Combined Work and reverse +engineering for debugging such modifications, if you also do each of +the following: + + a) Give prominent notice with each copy of the Combined Work that + the Library is used in it and that the Library and its use are + covered by this License. + + b) Accompany the Combined Work with a copy of the GNU GPL and this license + document. + + c) For a Combined Work that displays copyright notices during + execution, include the copyright notice for the Library among + these notices, as well as a reference directing the user to the + copies of the GNU GPL and this license document. + + d) Do one of the following: + + 0) Convey the Minimal Corresponding Source under the terms of this + License, and the Corresponding Application Code in a form + suitable for, and under terms that permit, the user to + recombine or relink the Application with a modified version of + the Linked Version to produce a modified Combined Work, in the + manner specified by section 6 of the GNU GPL for conveying + Corresponding Source. + + 1) Use a suitable shared library mechanism for linking with the + Library. A suitable mechanism is one that (a) uses at run time + a copy of the Library already present on the user's computer + system, and (b) will operate properly with a modified version + of the Library that is interface-compatible with the Linked + Version. + + e) Provide Installation Information, but only if you would otherwise + be required to provide such information under section 6 of the + GNU GPL, and only to the extent that such information is + necessary to install and execute a modified version of the + Combined Work produced by recombining or relinking the + Application with a modified version of the Linked Version. (If + you use option 4d0, the Installation Information must accompany + the Minimal Corresponding Source and Corresponding Application + Code. If you use option 4d1, you must provide the Installation + Information in the manner specified by section 6 of the GNU GPL + for conveying Corresponding Source.) + + 5. Combined Libraries. + + You may place library facilities that are a work based on the +Library side by side in a single library together with other library +facilities that are not Applications and are not covered by this +License, and convey such a combined library under terms of your +choice, if you do both of the following: + + a) Accompany the combined library with a copy of the same work based + on the Library, uncombined with any other library facilities, + conveyed under the terms of this License. + + b) Give prominent notice with the combined library that part of it + is a work based on the Library, and explaining where to find the + accompanying uncombined form of the same work. + + 6. Revised Versions of the GNU Lesser General Public License. + + The Free Software Foundation may publish revised and/or new versions +of the GNU Lesser General Public License from time to time. Such new +versions will be similar in spirit to the present version, but may +differ in detail to address new problems or concerns. + + Each version is given a distinguishing version number. If the +Library as you received it specifies that a certain numbered version +of the GNU Lesser General Public License "or any later version" +applies to it, you have the option of following the terms and +conditions either of that published version or of any later version +published by the Free Software Foundation. If the Library as you +received it does not specify a version number of the GNU Lesser +General Public License, you may choose any version of the GNU Lesser +General Public License ever published by the Free Software Foundation. + + If the Library as you received it specifies that a proxy can decide +whether future versions of the GNU Lesser General Public License shall +apply, that proxy's public statement of acceptance of any version is +permanent authorization for you to choose that version for the +Library. diff --git a/LICENSE.md b/LICENSE.md deleted file mode 100644 index 65c5ca8..0000000 --- a/LICENSE.md +++ /dev/null @@ -1,165 +0,0 @@ - GNU LESSER GENERAL PUBLIC LICENSE - Version 3, 29 June 2007 - - Copyright (C) 2007 Free Software Foundation, Inc. - Everyone is permitted to copy and distribute verbatim copies - of this license document, but changing it is not allowed. - - - This version of the GNU Lesser General Public License incorporates -the terms and conditions of version 3 of the GNU General Public -License, supplemented by the additional permissions listed below. - - 0. Additional Definitions. - - As used herein, "this License" refers to version 3 of the GNU Lesser -General Public License, and the "GNU GPL" refers to version 3 of the GNU -General Public License. - - "The Library" refers to a covered work governed by this License, -other than an Application or a Combined Work as defined below. - - An "Application" is any work that makes use of an interface provided -by the Library, but which is not otherwise based on the Library. -Defining a subclass of a class defined by the Library is deemed a mode -of using an interface provided by the Library. - - A "Combined Work" is a work produced by combining or linking an -Application with the Library. The particular version of the Library -with which the Combined Work was made is also called the "Linked -Version". - - The "Minimal Corresponding Source" for a Combined Work means the -Corresponding Source for the Combined Work, excluding any source code -for portions of the Combined Work that, considered in isolation, are -based on the Application, and not on the Linked Version. - - The "Corresponding Application Code" for a Combined Work means the -object code and/or source code for the Application, including any data -and utility programs needed for reproducing the Combined Work from the -Application, but excluding the System Libraries of the Combined Work. - - 1. Exception to Section 3 of the GNU GPL. - - You may convey a covered work under sections 3 and 4 of this License -without being bound by section 3 of the GNU GPL. - - 2. Conveying Modified Versions. - - If you modify a copy of the Library, and, in your modifications, a -facility refers to a function or data to be supplied by an Application -that uses the facility (other than as an argument passed when the -facility is invoked), then you may convey a copy of the modified -version: - - a) under this License, provided that you make a good faith effort to - ensure that, in the event an Application does not supply the - function or data, the facility still operates, and performs - whatever part of its purpose remains meaningful, or - - b) under the GNU GPL, with none of the additional permissions of - this License applicable to that copy. - - 3. Object Code Incorporating Material from Library Header Files. - - The object code form of an Application may incorporate material from -a header file that is part of the Library. You may convey such object -code under terms of your choice, provided that, if the incorporated -material is not limited to numerical parameters, data structure -layouts and accessors, or small macros, inline functions and templates -(ten or fewer lines in length), you do both of the following: - - a) Give prominent notice with each copy of the object code that the - Library is used in it and that the Library and its use are - covered by this License. - - b) Accompany the object code with a copy of the GNU GPL and this license - document. - - 4. Combined Works. - - You may convey a Combined Work under terms of your choice that, -taken together, effectively do not restrict modification of the -portions of the Library contained in the Combined Work and reverse -engineering for debugging such modifications, if you also do each of -the following: - - a) Give prominent notice with each copy of the Combined Work that - the Library is used in it and that the Library and its use are - covered by this License. - - b) Accompany the Combined Work with a copy of the GNU GPL and this license - document. - - c) For a Combined Work that displays copyright notices during - execution, include the copyright notice for the Library among - these notices, as well as a reference directing the user to the - copies of the GNU GPL and this license document. - - d) Do one of the following: - - 0) Convey the Minimal Corresponding Source under the terms of this - License, and the Corresponding Application Code in a form - suitable for, and under terms that permit, the user to - recombine or relink the Application with a modified version of - the Linked Version to produce a modified Combined Work, in the - manner specified by section 6 of the GNU GPL for conveying - Corresponding Source. - - 1) Use a suitable shared library mechanism for linking with the - Library. A suitable mechanism is one that (a) uses at run time - a copy of the Library already present on the user's computer - system, and (b) will operate properly with a modified version - of the Library that is interface-compatible with the Linked - Version. - - e) Provide Installation Information, but only if you would otherwise - be required to provide such information under section 6 of the - GNU GPL, and only to the extent that such information is - necessary to install and execute a modified version of the - Combined Work produced by recombining or relinking the - Application with a modified version of the Linked Version. (If - you use option 4d0, the Installation Information must accompany - the Minimal Corresponding Source and Corresponding Application - Code. If you use option 4d1, you must provide the Installation - Information in the manner specified by section 6 of the GNU GPL - for conveying Corresponding Source.) - - 5. Combined Libraries. - - You may place library facilities that are a work based on the -Library side by side in a single library together with other library -facilities that are not Applications and are not covered by this -License, and convey such a combined library under terms of your -choice, if you do both of the following: - - a) Accompany the combined library with a copy of the same work based - on the Library, uncombined with any other library facilities, - conveyed under the terms of this License. - - b) Give prominent notice with the combined library that part of it - is a work based on the Library, and explaining where to find the - accompanying uncombined form of the same work. - - 6. Revised Versions of the GNU Lesser General Public License. - - The Free Software Foundation may publish revised and/or new versions -of the GNU Lesser General Public License from time to time. Such new -versions will be similar in spirit to the present version, but may -differ in detail to address new problems or concerns. - - Each version is given a distinguishing version number. If the -Library as you received it specifies that a certain numbered version -of the GNU Lesser General Public License "or any later version" -applies to it, you have the option of following the terms and -conditions either of that published version or of any later version -published by the Free Software Foundation. If the Library as you -received it does not specify a version number of the GNU Lesser -General Public License, you may choose any version of the GNU Lesser -General Public License ever published by the Free Software Foundation. - - If the Library as you received it specifies that a proxy can decide -whether future versions of the GNU Lesser General Public License shall -apply, that proxy's public statement of acceptance of any version is -permanent authorization for you to choose that version for the -Library. -- cgit v1.2.3 From a7b46d4b0204571ba9124accebc84f77ae0bed26 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Thu, 30 Aug 2018 00:45:08 +0200 Subject: Add leq relation to meta-ordinals, it helps with proofs --- Empty.thy | 2 +- HoTT_Base.thy | 17 +++++++++++------ 2 files changed, 12 insertions(+), 7 deletions(-) diff --git a/Empty.thy b/Empty.thy index 1b339ba..8f5cc8c 100644 --- a/Empty.thy +++ b/Empty.thy @@ -17,7 +17,7 @@ axiomatization Empty :: Term ("\") and indEmpty :: "Term \ Term" ("(1ind\<^sub>\)") where - Empty_form: "\ : U(O)" + Empty_form: "\: U(O)" and Empty_elim: "\C: \ \ U(i); z: \\ \ ind\<^sub>\(z): C(z)" diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 1110e14..269a3d9 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -35,13 +35,18 @@ typedecl Ord axiomatization O :: Ord and S :: "Ord \ Ord" ("S_" [0] 1000) and - lt :: "[Ord, Ord] \ prop" (infix "<-" 999) + lt :: "[Ord, Ord] \ prop" (infix "<" 999) and + leq :: "[Ord, Ord] \ prop" (infix "\" 999) where - Ord_min: "\n. O <- S(n)" + Ord_lt_min: "\n. O < S(n)" and - Ord_monotone: "\m n. m <- n \ S(m) <- S(n)" + Ord_lt_monotone: "\m n. m < n \ S(m) < S(n)" +and + Ord_leq_min: "\n. n \ n" +and + Ord_leq_monotone: "\m n. m \ n \ S(m) \ S(n)" -lemmas Ord_rules [intro] = Ord_min Ord_monotone +lemmas Ord_rules [intro] = Ord_lt_min Ord_lt_monotone Ord_leq_min Ord_leq_monotone \ \Enables \standard\ to automatically solve inequalities.\ text "Define the universe types." @@ -49,9 +54,9 @@ text "Define the universe types." axiomatization U :: "Ord \ Term" where - U_hierarchy: "\i j. i <- j \ U(i): U(j)" + U_hierarchy: "\i j. i < j \ U(i): U(j)" and - U_cumulative: "\A i j. \A: U(i); i <- j\ \ A: U(j)" + U_cumulative: "\A i j. \A: U(i); i \ j\ \ A: U(j)" \ \WARNING: \rule Universe_cumulative\ can result in an infinite rewrite loop!\ -- cgit v1.2.3 From 2a2e8e46e0de6f99154a9421f75ae802557f22c7 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Thu, 30 Aug 2018 00:51:48 +0200 Subject: Should write the correct rule for Ord_leq_min. Another exercise. --- HoTT_Base.thy | 8 ++++++-- ex/HoTT book/Ch1.thy | 12 ++++++++++++ 2 files changed, 18 insertions(+), 2 deletions(-) diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 269a3d9..be4899c 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -42,7 +42,7 @@ where and Ord_lt_monotone: "\m n. m < n \ S(m) < S(n)" and - Ord_leq_min: "\n. n \ n" + Ord_leq_min: "\n. O \ n" and Ord_leq_monotone: "\m n. m \ n \ S(m) \ S(n)" @@ -57,7 +57,11 @@ where U_hierarchy: "\i j. i < j \ U(i): U(j)" and U_cumulative: "\A i j. \A: U(i); i \ j\ \ A: U(j)" - \ \WARNING: \rule Universe_cumulative\ can result in an infinite rewrite loop!\ + +text " + The rule \U_cumulative\ is very unsafe: if used as-is it will usually lead to an infinite rewrite loop! + It should be instantiated with the right ordinals \i\ and \j\ before being applied. +" section \Type families\ diff --git a/ex/HoTT book/Ch1.thy b/ex/HoTT book/Ch1.thy index d5f05dd..a577fca 100644 --- a/ex/HoTT book/Ch1.thy +++ b/ex/HoTT book/Ch1.thy @@ -40,4 +40,16 @@ proof (rule Sum_elim[where ?p=p]) qed (derive lems: assms) +section \Exercises\ + +text "Exercise 1.13" + +abbreviation "not" ("\'(_')") where "\(A) \ A \ \" + +text "This proof requires the use of universe cumulativity." + +proposition assumes "A: U(i)" shows "\<^bold>\f. f`(inr(\<^bold>\a. f`inl(a))): \(\(A + \(A)))" +by (derive lems: assms U_cumulative[where ?A=\ and ?i=O and ?j=i]) + + end -- cgit v1.2.3 From 2b42b190b15dcf74f033347604ea5530f3428364 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Thu, 30 Aug 2018 00:53:09 +0200 Subject: Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 4747be7..68ede63 100644 --- a/README.md +++ b/README.md @@ -4,7 +4,7 @@ An experimental implementation of [homotopy type theory](https://en.wikipedia.or ### Installation & Usage -Clone the contents of this repository into `/src/HoTT`. +Clone the contents of this repository into `/src/Isabelle-HoTT`. To use, set Isabelle's prover to Pure in the Theories panel, and import `HoTT`. -- cgit v1.2.3 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 +++++++++++++++++++++++++++++++++++++++++++++++++++++++- HoTT_Base.thy | 2 +- 2 files changed, 56 insertions(+), 2 deletions(-) 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 diff --git a/HoTT_Base.thy b/HoTT_Base.thy index be4899c..4e1a9be 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -60,7 +60,7 @@ and text " The rule \U_cumulative\ is very unsafe: if used as-is it will usually lead to an infinite rewrite loop! - It should be instantiated with the right ordinals \i\ and \j\ before being applied. + To avoid this, it should be instantiated before being applied. " -- 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 --- Coprod.thy | 34 +++++++++++------------ Empty.thy | 4 +-- Equal.thy | 22 +++++++-------- EqualProps.thy | 85 +++++++++++++++++++++++++++++----------------------------- HoTT_Base.thy | 14 +++++----- Nat.thy | 28 +++++++++---------- Prod.thy | 22 +++++++-------- ProdProps.thy | 12 ++++----- Proj.thy | 28 +++++++++---------- Sum.thy | 24 ++++++++--------- Unit.thy | 4 +-- 11 files changed, 138 insertions(+), 139 deletions(-) diff --git a/Coprod.thy b/Coprod.thy index 4607d1d..b87958a 100644 --- a/Coprod.thy +++ b/Coprod.thy @@ -17,40 +17,40 @@ axiomatization inr :: "Term \ Term" and indCoprod :: "[Term \ Term, Term \ Term, Term] \ Term" ("(1ind\<^sub>+)") where - Coprod_form: "\A: U(i); B: U(i)\ \ A + B: U(i)" + Coprod_form: "\A: U i; B: U i\ \ A + B: U i" and - Coprod_intro_inl: "\a: A; B: U(i)\ \ inl(a): A + B" + Coprod_intro_inl: "\a: A; B: U i\ \ inl a: A + B" and - Coprod_intro_inr: "\b: B; A: U(i)\ \ inr(b): A + B" + Coprod_intro_inr: "\b: B; A: U i\ \ inr b: A + B" and Coprod_elim: "\ - C: A + B \ U(i); - \x. x: A \ c(x): C(inl(x)); - \y. y: B \ d(y): C(inr(y)); + C: A + B \ U i; + \x. x: A \ c x: C (inl x); + \y. y: B \ d y: C (inr y); u: A + B - \ \ ind\<^sub>+(c)(d)(u) : C(u)" + \ \ ind\<^sub>+ c d u : C u" and Coprod_comp_inl: "\ - C: A + B \ U(i); - \x. x: A \ c(x): C(inl(x)); - \y. y: B \ d(y): C(inr(y)); + C: A + B \ U i; + \x. x: A \ c x: C (inl x); + \y. y: B \ d y: C (inr y); a: A - \ \ ind\<^sub>+(c)(d)(inl(a)) \ c(a)" + \ \ ind\<^sub>+ c d (inl a) \ c a" and Coprod_comp_inr: "\ - C: A + B \ U(i); - \x. x: A \ c(x): C(inl(x)); - \y. y: B \ d(y): C(inr(y)); + C: A + B \ U i; + \x. x: A \ c x: C (inl x); + \y. y: B \ d y: C (inr y); b: B - \ \ ind\<^sub>+(c)(d)(inr(b)) \ d(b)" + \ \ ind\<^sub>+ c d (inr b) \ d b" text "Admissible formation inference rules:" axiomatization where - Coprod_wellform1: "A + B: U(i) \ A: U(i)" + Coprod_wellform1: "A + B: U i \ A: U i" and - Coprod_wellform2: "A + B: U(i) \ B: U(i)" + Coprod_wellform2: "A + B: U i \ B: U i" text "Rule attribute declarations:" diff --git a/Empty.thy b/Empty.thy index 8f5cc8c..a42f7ff 100644 --- a/Empty.thy +++ b/Empty.thy @@ -17,9 +17,9 @@ axiomatization Empty :: Term ("\") and indEmpty :: "Term \ Term" ("(1ind\<^sub>\)") where - Empty_form: "\: U(O)" + Empty_form: "\: U O" and - Empty_elim: "\C: \ \ U(i); z: \\ \ ind\<^sub>\(z): C(z)" + Empty_elim: "\C: \ \ U i; z: \\ \ ind\<^sub>\ z: C z" text "Rule attribute declarations:" diff --git a/Equal.thy b/Equal.thy index 772072a..7254104 100644 --- a/Equal.thy +++ b/Equal.thy @@ -27,33 +27,33 @@ translations section \Type rules\ axiomatization where - Equal_form: "\A: U(i); a: A; b: A\ \ a =\<^sub>A b : U(i)" + Equal_form: "\A: U i; a: A; b: A\ \ a =\<^sub>A b : U i" and - Equal_intro: "a : A \ refl(a): a =\<^sub>A a" + Equal_intro: "a : A \ (refl a): a =\<^sub>A a" and Equal_elim: "\ x: A; y: A; p: x =\<^sub>A y; - \x. x: A \ f(x) : C(x)(x)(refl x); - \x y. \x: A; y: A\ \ C(x)(y): x =\<^sub>A y \ U(i) - \ \ ind\<^sub>=(f)(p) : C(x)(y)(p)" + \x. x: A \ f x: C x x (refl x); + \x y. \x: A; y: A\ \ C x y: x =\<^sub>A y \ U i + \ \ ind\<^sub>= f p : C x y p" and Equal_comp: "\ a: A; - \x. x: A \ f(x) : C(x)(x)(refl x); - \x y. \x: A; y: A\ \ C(x)(y): x =\<^sub>A y \ U(i) - \ \ ind\<^sub>=(f)(refl(a)) \ f(a)" + \x. x: A \ f x: C x x (refl x); + \x y. \x: A; y: A\ \ C x y: x =\<^sub>A y \ U i + \ \ ind\<^sub>= f (refl a) \ f a" text "Admissible inference rules for equality type formation:" axiomatization where - Equal_wellform1: "a =\<^sub>A b: U(i) \ A: U(i)" + Equal_wellform1: "a =\<^sub>A b: U i \ A: U i" and - Equal_wellform2: "a =\<^sub>A b: U(i) \ a: A" + Equal_wellform2: "a =\<^sub>A b: U i \ a: A" and - Equal_wellform3: "a =\<^sub>A b: U(i) \ b: A" + Equal_wellform3: "a =\<^sub>A b: U i \ b: A" text "Rule attribute declarations:" 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 diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 4e1a9be..a5b88fd 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -16,8 +16,6 @@ text "Meta syntactic type for object-logic types and terms." typedecl Term -section \Judgments\ - text " Formalize the typing judgment \a: A\. For judgmental/definitional equality we use the existing Pure equality \\\ and hence do not need to define a separate judgment for it. @@ -38,13 +36,13 @@ axiomatization lt :: "[Ord, Ord] \ prop" (infix "<" 999) and leq :: "[Ord, Ord] \ prop" (infix "\" 999) where - Ord_lt_min: "\n. O < S(n)" + Ord_lt_min: "\n. O < S n" and - Ord_lt_monotone: "\m n. m < n \ S(m) < S(n)" + Ord_lt_monotone: "\m n. m < n \ S m < S n" and Ord_leq_min: "\n. O \ n" and - Ord_leq_monotone: "\m n. m \ n \ S(m) \ S(n)" + Ord_leq_monotone: "\m n. m \ n \ S m \ S n" lemmas Ord_rules [intro] = Ord_lt_min Ord_lt_monotone Ord_leq_min Ord_leq_monotone \ \Enables \standard\ to automatically solve inequalities.\ @@ -54,9 +52,9 @@ text "Define the universe types." axiomatization U :: "Ord \ Term" where - U_hierarchy: "\i j. i < j \ U(i): U(j)" + U_hierarchy: "\i j. i < j \ U i: U j" and - U_cumulative: "\A i j. \A: U(i); i \ j\ \ A: U(j)" + U_cumulative: "\A i j. \A: U i; i \ j\ \ A: U j" text " The rule \U_cumulative\ is very unsafe: if used as-is it will usually lead to an infinite rewrite loop! @@ -71,7 +69,7 @@ text " " abbreviation (input) constrained :: "[Term \ Term, Term, Term] \ prop" ("(1_: _ \ _)") - where "f: A \ B \ (\x. x : A \ f(x): B)" + where "f: A \ B \ (\x. x : A \ f x: B)" text " The above is used to define type families, which are constrained meta-lambdas \P: A \ B\ where \A\ and \B\ are small types. diff --git a/Nat.thy b/Nat.thy index 45c3a2e..e879c92 100644 --- a/Nat.thy +++ b/Nat.thy @@ -17,31 +17,31 @@ axiomatization succ :: "Term \ Term" and indNat :: "[[Term, Term] \ Term, Term, Term] \ Term" ("(1ind\<^sub>\)") where - Nat_form: "\: U(O)" + Nat_form: "\: U O" and Nat_intro_0: "0: \" and - Nat_intro_succ: "n: \ \ succ(n): \" + Nat_intro_succ: "n: \ \ succ n: \" and Nat_elim: "\ - C: \ \ U(i); - \n c. \n: \; c: C(n)\ \ f(n)(c): C(succ n); - a: C(0); + C: \ \ U i; + \n c. \n: \; c: C n\ \ f n c: C (succ n); + a: C 0; n: \ - \ \ ind\<^sub>\(f)(a)(n): C(n)" + \ \ ind\<^sub>\ f a n: C n" and Nat_comp_0: "\ - C: \ \ U(i); - \n c. \n: \; c: C(n)\ \ f(n)(c): C(succ n); - a: C(0) - \ \ ind\<^sub>\(f)(a)(0) \ a" + C: \ \ U i; + \n c. \n: \; c: C(n)\ \ f n c: C (succ n); + a: C 0 + \ \ ind\<^sub>\ f a 0 \ a" and Nat_comp_succ: "\ - C: \ \ U(i); - \n c. \n: \; c: C(n)\ \ f(n)(c): C(succ n); - a: C(0); + C: \ \ U i; + \n c. \n: \; c: C n\ \ f n c: C (succ n); + a: C 0; n: \ - \ \ ind\<^sub>\(f)(a)(succ n) \ f(n)(ind\<^sub>\ f a n)" + \ \ ind\<^sub>\ f a (succ n) \ f n (ind\<^sub>\ f a n)" text "Rule attribute declarations:" diff --git a/Prod.thy b/Prod.thy index b0408b9..35d6b07 100644 --- a/Prod.thy +++ b/Prod.thy @@ -36,17 +36,17 @@ abbreviation Function :: "[Term, Term] \ Term" (infixr "\Type rules\ axiomatization where - Prod_form: "\A: U(i); B: A \ U(i)\ \ \x:A. B(x): U(i)" + Prod_form: "\A: U i; B: A \ U i\ \ \x:A. B x: U i" and - Prod_intro: "\\x. x: A \ b(x): B(x); A: U(i)\ \ \<^bold>\x. b(x): \x:A. B(x)" + Prod_intro: "\\x. x: A \ b x: B x; A: U i\ \ \<^bold>\x. b x: \x:A. B x" and - Prod_elim: "\f: \x:A. B(x); a: A\ \ f`a: B(a)" + Prod_elim: "\f: \x:A. B x; a: A\ \ f`a: B a" and - Prod_appl: "\\x. x: A \ b(x): B(x); a: A\ \ (\<^bold>\x. b(x))`a \ b(a)" + Prod_appl: "\\x. x: A \ b x: B x; a: A\ \ (\<^bold>\x. b x)`a \ b a" and - Prod_uniq: "f : \x:A. B(x) \ \<^bold>\x. (f`x) \ f" + Prod_uniq: "f : \x:A. B x \ \<^bold>\x. (f`x) \ f" and - Prod_eq: "\\x. x: A \ b(x) \ b'(x); A: U(i)\ \ \<^bold>\x. b(x) \ \<^bold>\x. b'(x)" + Prod_eq: "\\x. x: A \ b x \ c x; A: U i\ \ \<^bold>\x. b x \ \<^bold>\x. c x" text " The Pure rules for \\\ only let us judge strict syntactic equality of object lambda expressions; Prod_eq is the actual definitional equality rule. @@ -55,15 +55,15 @@ text " " text " - In addition to the usual type rules, it is a meta-theorem that whenever \\x:A. B x: U(i)\ is derivable from some set of premises \, then so are \A: U(i)\ and \B: A \ U(i)\. + In addition to the usual type rules, it is a meta-theorem that whenever \\x:A. B x: U i\ is derivable from some set of premises \, then so are \A: U i\ and \B: A \ U i\. That is to say, the following inference rules are admissible, and it simplifies proofs greatly to axiomatize them directly. " axiomatization where - Prod_wellform1: "(\x:A. B(x): U(i)) \ A: U(i)" + Prod_wellform1: "(\x:A. B x: U i) \ A: U i" and - Prod_wellform2: "(\x:A. B(x): U(i)) \ B: A \ U(i)" + Prod_wellform2: "(\x:A. B x: U i) \ B: A \ U i" text "Rule attribute declarations---set up various methods to use the type rules." @@ -75,9 +75,9 @@ lemmas Prod_routine [intro] = Prod_form Prod_intro Prod_elim section \Function composition\ -definition compose :: "[Term, Term] \ Term" (infixr "o" 70) where "g o f \ \<^bold>\x. g`(f`x)" +definition compose :: "[Term, Term] \ Term" (infixr "o" 110) where "g o f \ \<^bold>\x. g`(f`x)" -syntax "_COMPOSE" :: "[Term, Term] \ Term" (infixr "\" 70) +syntax "_COMPOSE" :: "[Term, Term] \ Term" (infixr "\" 110) translations "g \ f" \ "g o f" diff --git a/ProdProps.thy b/ProdProps.thy index 1af6ad3..14556af 100644 --- a/ProdProps.thy +++ b/ProdProps.thy @@ -18,7 +18,7 @@ text " " lemma compose_assoc: - assumes "A: U(i)" and "f: A \ B" "g: B \ C" "h: \x:C. D(x)" + assumes "A: U i" and "f: A \ B" "g: B \ C" "h: \x:C. D x" shows "(h \ g) \ f \ h \ (g \ f)" proof (subst (0 1 2 3) compose_def) show "\<^bold>\x. (\<^bold>\y. h`(g`y))`(f`x) \ \<^bold>\x. h`((\<^bold>\y. g`(f`y))`x)" @@ -31,19 +31,19 @@ proof (subst (0 1 2 3) compose_def) proof compute show "\x. x: A \ g`(f`x): C" by (routine lems: assms) qed - show "\x. x: B \ h`(g`x): D(g`x)" by (routine lems: assms) + show "\x. x: B \ h`(g`x): D (g`x)" by (routine lems: assms) qed (routine lems: assms) qed fact qed lemma compose_comp: - assumes "A: U(i)" and "\x. x: A \ b(x): B" and "\x. x: B \ c(x): C(x)" - shows "(\<^bold>\x. c(x)) \ (\<^bold>\x. b(x)) \ \<^bold>\x. c(b(x))" + assumes "A: U i" and "\x. x: A \ b x: B" and "\x. x: B \ c x: C x" + shows "(\<^bold>\x. c x) \ (\<^bold>\x. b x) \ \<^bold>\x. c (b x)" proof (subst compose_def, subst Prod_eq) - show "\a. a: A \ (\<^bold>\x. c(x))`((\<^bold>\x. b(x))`a) \ (\<^bold>\x. c (b x))`a" + show "\a. a: A \ (\<^bold>\x. c x)`((\<^bold>\x. b x)`a) \ (\<^bold>\x. c (b x))`a" proof compute - show "\a. a: A \ c((\<^bold>\x. b(x))`a) \ (\<^bold>\x. c(b(x)))`a" + show "\a. a: A \ c ((\<^bold>\x. b x)`a) \ (\<^bold>\x. c (b x))`a" by (derive lems: assms) qed (routine lems: assms) qed (derive lems: assms) diff --git a/Proj.thy b/Proj.thy index a1c4c8f..74c561c 100644 --- a/Proj.thy +++ b/Proj.thy @@ -12,44 +12,44 @@ theory Proj begin -definition fst :: "Term \ Term" where "fst(p) \ ind\<^sub>\ (\x y. x) p" -definition snd :: "Term \ Term" where "snd(p) \ ind\<^sub>\ (\x y. y) p" +definition fst :: "Term \ Term" where "fst p \ ind\<^sub>\ (\x y. x) p" +definition snd :: "Term \ Term" where "snd p \ ind\<^sub>\ (\x y. y) p" text "Typing judgments and computation rules for the dependent and non-dependent projection functions." lemma fst_type: - assumes "\x:A. B(x): U(i)" and "p: \x:A. B(x)" shows "fst(p): A" + assumes "\x:A. B x: U i" and "p: \x:A. B x" shows "fst p: A" unfolding fst_def by (derive lems: assms) lemma fst_comp: - assumes "A: U(i)" and "B: A \ U(i)" and "a: A" and "b: B(a)" shows "fst() \ a" + assumes "A: U i" and "B: A \ U i" and "a: A" and "b: B a" shows "fst \ a" unfolding fst_def proof compute - show "a: A" and "b: B(a)" by fact+ + show "a: A" and "b: B a" by fact+ qed (routine lems: assms)+ lemma snd_type: - assumes "\x:A. B(x): U(i)" and "p: \x:A. B(x)" shows "snd(p): B(fst p)" + assumes "\x:A. B x: U i" and "p: \x:A. B x" shows "snd p: B (fst p)" unfolding snd_def proof - show "\p. p: \x:A. B(x) \ B(fst p): U(i)" by (derive lems: assms fst_type) + show "\p. p: \x:A. B x \ B (fst p): U i" by (derive lems: assms fst_type) fix x y - assume asm: "x: A" "y: B(x)" - show "y: B(fst )" + assume asm: "x: A" "y: B x" + show "y: B (fst )" proof (subst fst_comp) - show "A: U(i)" by (wellformed lems: assms(1)) - show "\x. x: A \ B(x): U(i)" by (wellformed lems: assms(1)) + show "A: U i" by (wellformed lems: assms(1)) + show "\x. x: A \ B x: U i" by (wellformed lems: assms(1)) qed fact+ qed fact lemma snd_comp: - assumes "A: U(i)" and "B: A \ U(i)" and "a: A" and "b: B(a)" shows "snd() \ b" + assumes "A: U i" and "B: A \ U i" and "a: A" and "b: B a" shows "snd \ b" unfolding snd_def proof compute - show "\x y. y: B(x) \ y: B(x)" . + show "\x y. y: B x \ y: B x" . show "a: A" by fact - show "b: B(a)" by fact + show "b: B a" by fact qed (routine lems: assms) diff --git a/Sum.thy b/Sum.thy index 8d0b0e6..6de20fd 100644 --- a/Sum.thy +++ b/Sum.thy @@ -33,30 +33,30 @@ abbreviation Pair :: "[Term, Term] \ Term" (infixr "\" 50) section \Type rules\ axiomatization where - Sum_form: "\A: U(i); B: A \ U(i)\ \ \x:A. B(x): U(i)" + Sum_form: "\A: U i; B: A \ U i\ \ \x:A. B x: U i" and - Sum_intro: "\B: A \ U(i); a: A; b: B(a)\ \ : \x:A. B(x)" + Sum_intro: "\B: A \ U i; a: A; b: B a\ \ : \x:A. B x" and Sum_elim: "\ - p: \x:A. B(x); - \x y. \x: A; y: B(x)\ \ f(x)(y): C(); - C: \x:A. B(x) \ U(i) - \ \ ind\<^sub>\(f)(p): C(p)" (* What does writing \x y. f(x, y) change? *) + p: \x:A. B x; + \x y. \x: A; y: B x\ \ f x y: C ; + C: \x:A. B x \ U i + \ \ ind\<^sub>\ f p: C p" (* What does writing \x y. f(x, y) change? *) and Sum_comp: "\ a: A; - b: B(a); - \x y. \x: A; y: B(x)\ \ f(x)(y): C(); + b: B a; + \x y. \x: A; y: B(x)\ \ f x y: C ; B: A \ U(i); - C: \x:A. B(x) \ U(i) - \ \ ind\<^sub>\(f)() \ f(a)(b)" + C: \x:A. B x \ U i + \ \ ind\<^sub>\ f \ f a b" text "Admissible inference rules for sum formation:" axiomatization where - Sum_wellform1: "(\x:A. B(x): U(i)) \ A: U(i)" + Sum_wellform1: "(\x:A. B x: U i) \ A: U i" and - Sum_wellform2: "(\x:A. B(x): U(i)) \ B: A \ U(i)" + Sum_wellform2: "(\x:A. B x: U i) \ B: A \ U i" text "Rule attribute declarations:" diff --git a/Unit.thy b/Unit.thy index 6adfb02..9b86739 100644 --- a/Unit.thy +++ b/Unit.thy @@ -20,9 +20,9 @@ where and Unit_intro: "\: \" and - Unit_elim: "\C: \ \ U(i); c: C(\); a: \\ \ ind\<^sub>\(c)(a) : C(a)" + Unit_elim: "\C: \ \ U i; c: C \; a: \\ \ ind\<^sub>\ c a: C a" and - Unit_comp: "\C: \ \ U(i); c: C(\)\ \ ind\<^sub>\(c)(\) \ c" + Unit_comp: "\C: \ \ U i; c: C \\ \ ind\<^sub>\ c \ \ c" text "Rule attribute declarations:" -- 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 +++++ Prod.thy | 5 +++++ Univalence.thy | 71 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 81 insertions(+) create mode 100644 Univalence.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 diff --git a/Prod.thy b/Prod.thy index 35d6b07..a7968b6 100644 --- a/Prod.thy +++ b/Prod.thy @@ -81,4 +81,9 @@ syntax "_COMPOSE" :: "[Term, Term] \ Term" (infixr "\" 110) translations "g \ f" \ "g o f" +section \Polymorphic identity function\ + +abbreviation id :: Term where "id \ \<^bold>\x. x" + + end diff --git a/Univalence.thy b/Univalence.thy new file mode 100644 index 0000000..b999a55 --- /dev/null +++ b/Univalence.thy @@ -0,0 +1,71 @@ +(* Title: HoTT/Univalence.thy + Author: Josh Chen + +Definitions of homotopy, equivalence and the univalence axiom. +*) + +theory Univalence + imports + HoTT_Methods + Equal + ProdProps + Sum +begin + + +section \Homotopy and equivalence\ + +axiomatization homotopic :: "[Term, Term] \ Term" (infix "~" 100) where + homotopic_def: "\ + f: \x:A. B x; + g: \x:A. B x + \ \ f ~ g \ \x:A. (f`x) =[B x] (g`x)" + +axiomatization isequiv :: "Term \ Term" where + isequiv_def: "f: A \ B \ isequiv f \ (\g: A \ B. g \ f ~ id) \ (\g: A \ B. f \ g ~ id)" + +definition equivalence :: "[Term, Term] \ Term" (infix "\" 100) + where "A \ B \ \f: A \ B. isequiv f" + + +text "The identity function is an equivalence:" + +lemma isequiv_id: + assumes "A: U i" and "id: A \ A" + shows "<\x. refl x>, \x. refl x>>: isequiv id" +proof (derive lems: assms isequiv_def homotopic_def) + fix g assume asm: "g: A \ A" + show "id \ g: A \ A" + unfolding compose_def by (derive lems: asm assms) + + show "\x:A. ((id \ g)`x) =\<^sub>A (id`x): U i" + unfolding compose_def by (derive lems: asm assms) + + next + show "<\<^bold>\x. x, \<^bold>\x. refl x>: \g:A \ A. (g \ id) ~ id" + unfolding compose_def by (derive lems: assms homotopic_def) + + show "<\<^bold>\x. x, lambda refl>: \g:A \ A. (id \ g) ~ id" + unfolding compose_def by (derive lems: assms homotopic_def) +qed (rule assms) + + +text "The equivalence relation \\\ is symmetric:" + +lemma + assumes "A: U i" and "id: A \ A" + shows "\x. refl x>, \x. refl x>>>: A \ A" +unfolding equivalence_def proof + show "<\x. refl x>, \x. refl x>>: isequiv id" using assms by (rule isequiv_id) + + fix f assume asm: "f: A \ A" show "isequiv f: U i" + by (derive lems: asm assms homotopic_def isequiv_def compose_def) +qed (rule assms) + + +text "Definition of \idtoeqv\:" + + + + +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 +++++++++++++ HoTT_Base.thy | 16 ++++++++------ Univalence.thy | 66 ++++++++++++++++++++++++++++++++++++++++++++++++---------- 3 files changed, 80 insertions(+), 17 deletions(-) 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 diff --git a/HoTT_Base.thy b/HoTT_Base.thy index a5b88fd..916f6aa 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -32,19 +32,23 @@ typedecl Ord axiomatization O :: Ord and - S :: "Ord \ Ord" ("S_" [0] 1000) and + S :: "Ord \ Ord" ("S _" [0] 1000) and lt :: "[Ord, Ord] \ prop" (infix "<" 999) and leq :: "[Ord, Ord] \ prop" (infix "\" 999) where - Ord_lt_min: "\n. O < S n" + lt_min: "\n. O < S n" and - Ord_lt_monotone: "\m n. m < n \ S m < S n" + lt_monotone1: "\n. n < S n" and - Ord_leq_min: "\n. O \ n" + lt_monotone2: "\m n. m < n \ S m < S n" and - Ord_leq_monotone: "\m n. m \ n \ S m \ S n" + leq_min: "\n. O \ n" +and + leq_monotone1: "\n. n \ S n" +and + leq_monotone2: "\m n. m \ n \ S m \ S n" -lemmas Ord_rules [intro] = Ord_lt_min Ord_lt_monotone Ord_leq_min Ord_leq_monotone +lemmas Ord_rules [intro] = lt_min lt_monotone1 lt_monotone2 leq_min leq_monotone1 leq_monotone2 \ \Enables \standard\ to automatically solve inequalities.\ text "Define the universe types." diff --git a/Univalence.thy b/Univalence.thy index b999a55..e16ea03 100644 --- a/Univalence.thy +++ b/Univalence.thy @@ -7,7 +7,7 @@ Definitions of homotopy, equivalence and the univalence axiom. theory Univalence imports HoTT_Methods - Equal + EqualProps ProdProps Sum begin @@ -22,7 +22,7 @@ axiomatization homotopic :: "[Term, Term] \ Term" (infix "~" 100) w \ \ f ~ g \ \x:A. (f`x) =[B x] (g`x)" axiomatization isequiv :: "Term \ Term" where - isequiv_def: "f: A \ B \ isequiv f \ (\g: A \ B. g \ f ~ id) \ (\g: A \ B. f \ g ~ id)" + isequiv_def: "f: A \ B \ isequiv f \ (\g: B \ A. g \ f ~ id) \ (\g: B \ A. f \ g ~ id)" definition equivalence :: "[Term, Term] \ Term" (infix "\" 100) where "A \ B \ \f: A \ B. isequiv f" @@ -36,12 +36,12 @@ lemma isequiv_id: proof (derive lems: assms isequiv_def homotopic_def) fix g assume asm: "g: A \ A" show "id \ g: A \ A" - unfolding compose_def by (derive lems: asm assms) + unfolding compose_def by (routine lems: asm assms) show "\x:A. ((id \ g)`x) =\<^sub>A (id`x): U i" - unfolding compose_def by (derive lems: asm assms) - + unfolding compose_def by (routine lems: asm assms) next + show "<\<^bold>\x. x, \<^bold>\x. refl x>: \g:A \ A. (g \ id) ~ id" unfolding compose_def by (derive lems: assms homotopic_def) @@ -50,22 +50,66 @@ proof (derive lems: assms isequiv_def homotopic_def) qed (rule assms) +text "We use the following lemma in a few proofs:" + +lemma isequiv_type: + assumes "A: U i" and "B: U i" and "f: A \ B" + shows "isequiv f: U i" + by (derive lems: assms isequiv_def homotopic_def compose_def) + + text "The equivalence relation \\\ is symmetric:" -lemma +lemma equiv_sym: assumes "A: U i" and "id: A \ A" shows "\x. refl x>, \x. refl x>>>: A \ A" unfolding equivalence_def proof show "<\x. refl x>, \x. refl x>>: isequiv id" using assms by (rule isequiv_id) - fix f assume asm: "f: A \ A" show "isequiv f: U i" - by (derive lems: asm assms homotopic_def isequiv_def compose_def) + fix f assume "f: A \ A" + with assms(1) assms(1) show "isequiv f: U i" by (rule isequiv_type) qed (rule assms) -text "Definition of \idtoeqv\:" - - +section \idtoeqv and the univalence axiom\ + +definition idtoeqv :: Term + where "idtoeqv \ \<^bold>\p. = (\A. <\x. refl x>, \x. refl x>>) p>" + +text "Equal types are equivalent. The proof uses universes." + +theorem + assumes "A: U i" and "B: U i" + shows "idtoeqv: (A =[U i] B) \ A \ B" +unfolding idtoeqv_def equivalence_def +proof + fix p assume "p: A =[U i] B" + show "= (\A. <\x. refl x>, \x. refl x>>) p>: \f: A \ B. isequiv f" + proof + { fix f assume "f: A \ B" + with assms show "isequiv f: U i" by (rule isequiv_type) + } + + show "transport p: A \ B" + proof (rule transport_type[where ?P="\x. x" and ?A="U i" and ?i="S i"]) + show "\x. x: U i \ x: U S i" by (elim U_cumulative) standard + show "U i: U S i" by (rule U_hierarchy) standard + qed fact+ + + show "ind\<^sub>= (\A. <\x. refl x>, \x. refl x>>) p: isequiv (transport p)" + proof (rule Equal_elim[where ?C="\_ _ p. isequiv (transport p)"]) + fix A assume asm: "A: U i" + show "<\x. refl x>, \x. refl x>>: isequiv (transport (refl A))" + proof (derive lems: isequiv_def) + show "transport (refl A): A \ A" + unfolding transport_def + by (compute lems: Equal_comp[where ?A="U i" and ?C="\_ _ _. A \ A"]) (derive lems: asm) + + show "<\x. refl x>, \x. refl x>>: + (\g:A \ A. g \ (transport (refl A)) ~ id) \ + (\g:A \ A. (transport (refl A)) \ g ~ id)" + proof (derive lems: asm homotopic_def transport_def) + show "id: A \ A" by (routine lems: asm) 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 ++ ProdProps.thy | 5 +++++ Univalence.thy | 68 ++++++++++++++++++++++++++++++++++++++++++++++++++++++---- 3 files changed, 71 insertions(+), 4 deletions(-) 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 diff --git a/ProdProps.thy b/ProdProps.thy index 14556af..47e386b 100644 --- a/ProdProps.thy +++ b/ProdProps.thy @@ -49,4 +49,9 @@ proof (subst compose_def, subst Prod_eq) qed (derive lems: assms) +text "Set up the \compute\ method to automatically simplify function compositions." + +lemmas compose_comp [comp] + + end diff --git a/Univalence.thy b/Univalence.thy index e16ea03..80325f3 100644 --- a/Univalence.thy +++ b/Univalence.thy @@ -76,7 +76,8 @@ section \idtoeqv and the univalence axiom\ definition idtoeqv :: Term where "idtoeqv \ \<^bold>\p. = (\A. <\x. refl x>, \x. refl x>>) p>" -text "Equal types are equivalent. The proof uses universes." + +text "We prove that equal types are equivalent. The proof is long and uses universes." theorem assumes "A: U i" and "B: U i" @@ -95,7 +96,7 @@ proof show "\x. x: U i \ x: U S i" by (elim U_cumulative) standard show "U i: U S i" by (rule U_hierarchy) standard qed fact+ - + show "ind\<^sub>= (\A. <\x. refl x>, \x. refl x>>) p: isequiv (transport p)" proof (rule Equal_elim[where ?C="\_ _ p. isequiv (transport p)"]) fix A assume asm: "A: U i" @@ -108,8 +109,67 @@ proof show "<\x. refl x>, \x. refl x>>: (\g:A \ A. g \ (transport (refl A)) ~ id) \ (\g:A \ A. (transport (refl A)) \ g ~ id)" - proof (derive lems: asm homotopic_def transport_def) - show "id: A \ A" by (routine lems: asm) + proof (subst (1 2) transport_comp) + show "U i: U S i" by (rule U_hierarchy) standard + show "U i: U S i" by (rule U_hierarchy) standard + + show "<\x. refl x>, \x. refl x>>: + (\g:A \ A. g \ id ~ id) \ (\g:A \ A. id \ g ~ id)" + proof + show "\g:A \ A. id \ g ~ id: U i" + proof (derive lems: asm homotopic_def) + fix g assume asm': "g: A \ A" + show *: "id \ g: A \ A" by (derive lems: asm asm' compose_def) + show "\x:A. ((id \ g)`x) =\<^sub>A (id`x): U i" by (derive lems: asm *) + qed (routine lems: asm) + + show "\x. refl x>: \g:A \ A. id \ g ~ id" + proof + fix g assume asm': "g: A \ A" + show "id \ g ~ id: U i" + proof (derive lems: homotopic_def) + show *: "id \ g: A \ A" by (derive lems: asm asm' compose_def) + show "\x:A. ((id \ g)`x) =\<^sub>A (id`x): U i" by (derive lems: asm *) + qed (routine lems: asm) + next + show "\<^bold>\x. refl x: id \ id ~ id" + proof compute + show "\<^bold>\x. refl x: id ~ id" by (subst homotopic_def) (derive lems: asm) + qed (rule asm) + qed (routine lems: asm) + + show "\x. refl x>: \g:A \ A. g \ id ~ id" + proof + fix g assume asm': "g: A \ A" + show "g \ id ~ id: U i" by (derive lems: asm asm' homotopic_def compose_def) + next + show "\<^bold>\x. refl x: id \ id ~ id" + proof compute + show "\<^bold>\x. refl x: id ~ id" by (subst homotopic_def) (derive lems: asm) + qed (rule asm) + qed (routine lems: asm) + qed + qed fact+ + qed + next + + fix A' B' p' assume asm: "A': U i" "B': U i" "p': A' =[U i] B'" + show "isequiv (transport p'): U i" + proof (rule isequiv_type) + show "transport p': A' \ B'" by (derive lems: asm transport_def) + qed fact+ + qed fact+ + qed + next + + show "A =[U i] B: U (S i)" by (derive lems: assms | rule U_hierarchy)+ +qed + + +text "The univalence axiom:" + +axiomatization univalence :: Term where + ua: "univalence: isequiv idtoeqv" end -- cgit v1.2.3 From 563510a1940024779c3e1f73df8c1b708eb0d949 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 11 Sep 2018 19:27:57 +0200 Subject: Update README.md --- README.md | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 68ede63..d557f3e 100644 --- a/README.md +++ b/README.md @@ -4,15 +4,19 @@ An experimental implementation of [homotopy type theory](https://en.wikipedia.or ### Installation & Usage -Clone the contents of this repository into `/src/Isabelle-HoTT`. +Clone or copy the contents of this repository into `/src/Isabelle-HoTT`. To use, set Isabelle's prover to Pure in the Theories panel, and import `HoTT`. +### Some comments on the implementation + +The implementation in the `master` branch is polymorphic without type annotations, and as such has some differences with the standard theory as presented in the [Homotopy Type Theory book](https://homotopytypetheory.org/book/). + ### Collaboration -I've been flying solo on this library as part of my Masters project, and there are very many improvements and developments that have yet to be implemented, so ***collaborators are welcome!*** +I've been flying solo on this library as part of my Masters project, and there are very many improvements and developments that have yet to be implemented, so **collaborators are welcome!** -If you're interested in working together on any part of this do drop me a line at `joshua DOT chen AT uni-bonn DOT de`. +If you're interested in working together on any part of this library do drop me a line at `joshua DOT chen AT uni-bonn DOT de`. ### License -- 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 --- Coprod.thy | 2 +- EqualProps.thy | 4 ++-- ProdProps.thy | 2 +- Sum.thy | 2 +- Unit.thy | 2 +- Univalence.thy | 4 +++- 6 files changed, 9 insertions(+), 7 deletions(-) diff --git a/Coprod.thy b/Coprod.thy index b87958a..1ff7361 100644 --- a/Coprod.thy +++ b/Coprod.thy @@ -28,7 +28,7 @@ and \x. x: A \ c x: C (inl x); \y. y: B \ d y: C (inr y); u: A + B - \ \ ind\<^sub>+ c d u : C u" + \ \ ind\<^sub>+ c d u: C u" and Coprod_comp_inl: "\ C: A + B \ U i; 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 diff --git a/ProdProps.thy b/ProdProps.thy index 47e386b..a68f79b 100644 --- a/ProdProps.thy +++ b/ProdProps.thy @@ -14,7 +14,7 @@ begin section \Composition\ text " - The proof of associativity needs some guidance; it involves telling Isabelle to use the correct rule for \-type definitional equality, and the correct substitutions in the subgoals thereafter. + The proof of associativity needs some guidance; it involves telling Isabelle to use the correct rule for \-type definitional equality, and the correct substitutions in the subgoals thereafter. " lemma compose_assoc: diff --git a/Sum.thy b/Sum.thy index 6de20fd..aac81f7 100644 --- a/Sum.thy +++ b/Sum.thy @@ -47,7 +47,7 @@ and a: A; b: B a; \x y. \x: A; y: B(x)\ \ f x y: C ; - B: A \ U(i); + B: A \ U i; C: \x:A. B x \ U i \ \ ind\<^sub>\ f \ f a b" diff --git a/Unit.thy b/Unit.thy index 9b86739..6760f27 100644 --- a/Unit.thy +++ b/Unit.thy @@ -16,7 +16,7 @@ axiomatization pt :: Term ("\") and indUnit :: "[Term, Term] \ Term" ("(1ind\<^sub>\)") where - Unit_form: "\: U(O)" + Unit_form: "\: U O" and Unit_intro: "\: \" and diff --git a/Univalence.thy b/Univalence.thy index 80325f3..8599ba7 100644 --- a/Univalence.thy +++ b/Univalence.thy @@ -15,6 +15,8 @@ begin section \Homotopy and equivalence\ +text "We define polymorphic constants implementing the definitions of homotopy and equivalence." + axiomatization homotopic :: "[Term, Term] \ Term" (infix "~" 100) where homotopic_def: "\ f: \x:A. B x; @@ -166,7 +168,7 @@ proof qed -text "The univalence axiom:" +text "The univalence axiom." axiomatization univalence :: Term where ua: "univalence: isequiv idtoeqv" -- cgit v1.2.3 From f0999d07a0f41284ba84fae725a0186e0ec9ff5f Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Wed, 12 Sep 2018 09:10:08 +0200 Subject: Final commit before first release --- Univalence.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Univalence.thy b/Univalence.thy index 8599ba7..b7f4400 100644 --- a/Univalence.thy +++ b/Univalence.thy @@ -171,7 +171,7 @@ qed text "The univalence axiom." axiomatization univalence :: Term where - ua: "univalence: isequiv idtoeqv" + UA: "univalence: isequiv idtoeqv" end -- cgit v1.2.3