From 602ad9fe0e2ed1ad4ab6f16e720de878aadc0fba Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Fri, 15 Jun 2018 17:17:27 +0200 Subject: projections --- HoTT_Base.thy | 40 +++++++++++++--------------------------- HoTT_Theorems.thy | 3 +++ Sum.thy | 41 ++++++++++++++++++++++++++++------------- 3 files changed, 44 insertions(+), 40 deletions(-) diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 9b422c4..7794601 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -2,7 +2,7 @@ Author: Josh Chen Date: Jun 2018 -Basic setup and definitions of a homotopy type theory object logic. +Basic setup and definitions of a homotopy type theory object logic without universes. *) theory HoTT_Base @@ -18,16 +18,23 @@ text "Set up type checking routines, proof methods etc." section \Metalogical definitions\ text "A single meta-type \Term\ suffices to implement the object-logic types and terms. -Our implementation does not have universes, and we simply use \a : U\ as a convenient shorthand meaning ``\a\ is a type''." +We do not implement universes, and simply use \a : U\ as a convenient shorthand to mean ``\a\ is a type''." typedecl Term section \Judgments\ +text "We formalize the judgments \a : A\ and \A : U\ separately, in contrast to the HoTT book where the latter is considered an instance of the former. + +For judgmental equality we use the existing Pure equality \\\ and hence do not need to define a separate judgment for it." + consts -is_a_type :: "Term \ prop" ("(1_ :/ U)" [0] 1000) -is_of_type :: "[Term, Term] \ prop" ("(1_ :/ _)" [0, 0] 1000) + is_a_type :: "Term \ prop" ("(1_ :/ U)" [0] 1000) + is_of_type :: "[Term, Term] \ prop" ("(1_ :/ _)" [0, 0] 1000) + +axiomatization where + inhabited_implies_type [intro]: "\a A. a : A \ A : U" section \Type families\ @@ -36,31 +43,10 @@ text "A (one-variable) type family is a meta lambda term \P :: Term \ prop" ("(3_:/ _ \ U)") +abbreviation (input) is_type_family :: "[Typefam, Term] \ prop" ("(3_:/ _ \ U)") where "P: A \ U \ (\x. x : A \ P x : U)" -text "There is an obvious generalization to multivariate type families, but implementing such an abbreviation involves writing ML and is for the moment not really crucial." - - -section \Definitional equality\ - -text "The Pure equality \\\ is used for definitional aka judgmental equality of types and terms." - -\ \Do these ever need to be used? - -theorem equal_types: - assumes "A \ B" and "A : U" - shows "B : U" using assms by simp - -theorem equal_type_element: - assumes "A \ B" and "x : A" - shows "x : B" using assms by simp +text "There is an obvious generalization to multivariate type families, but implementing such an abbreviation involves writing ML code, and is for the moment not really crucial." -lemmas type_equality = - equal_types - equal_types[rotated] - equal_type_element - equal_type_element[rotated] -\ end \ No newline at end of file diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy index 2c2a31d..ab5374d 100644 --- a/HoTT_Theorems.thy +++ b/HoTT_Theorems.thy @@ -34,6 +34,9 @@ proof fix a assume "a : A" then show "\<^bold>\y:B. a : B \ A" .. + + ML_val \@{context} |> Variable.names_of\ + qed diff --git a/Sum.thy b/Sum.thy index 8dab3e8..3db0f23 100644 --- a/Sum.thy +++ b/Sum.thy @@ -6,7 +6,7 @@ Dependent sum type. *) theory Sum - imports HoTT_Base Prod + imports Prod begin @@ -68,32 +68,47 @@ overloading snd_nondep \ snd begin definition snd_dep :: "[Term, Typefam] \ Term" where - "snd_dep A B \ indSum[A,B] (\p. B(fst[A,B]`p)) (\x y. y)" + "snd_dep A B \ indSum[A,B] (\p. B fst[A,B]`p) (\x y. y)" definition snd_nondep :: "[Term, Term] \ Term" where - "snd_nondep A B \ indSum[A, \_. B] (\p. B((fst A B)`p)) (\x y. y)" + "snd_nondep A B \ indSum[A, \_. B] (\_. B) (\x y. y)" end -text "Simplification rules:" +text "Properties of projections:" + +lemma fst_dep_type: + assumes "p : \x:A. B x" + shows "fst[A,B]`p : A" +proof - + have "\x:A. B x : U" using assms .. + then have "A : U" by (rule Sum_intro) + unfolding fst_dep_def using assms by (rule Sum_comp) + lemma fst_dep_comp: - assumes "a : A" and "b : B(a)" + assumes "a : A" and "b : B a" shows "fst[A,B]`(a,b) \ a" proof - - show "fst[A,B]`(a,b) \ a" unfolding fst_dep_def using assms by simp + have "A : U" using assms(1) .. + then have "\_. A: \x:A. B x \ U" . + moreover have "\x y. x : A \ (\x y. x) x y : A" . + ultimately show "fst[A,B]`(a,b) \ a" unfolding fst_dep_def using assms by (rule Sum_comp) qed -lemma snd_dep_comp: "\a : A; b : B(a)\ \ snd[A,B]`(a,b) \ b" +lemma snd_dep_comp: + assumes "a : A" and "b : B a" + shows "snd[A,B]`(a,b) \ b" proof - - assume "a : A" and "b : B(a)" - then have "(a, b) : \x:A. B(x)" .. - then show "snd[A,B]`(a,b) \ b" unfolding snd_dep_def by simp + have "\p. B fst[A,B]`p: \x:A. B x \ U" + + ultimately show "snd[A,B]`(a,b) \ b" unfolding snd_dep_def by (rule Sum_comp) qed -lemma fst_nondep_comp: "\a : A; b : B\ \ fst[A,B]`(a,b) \ a" +lemma fst_nondep_comp: + assumes "a : A" and "b : B" + shows "fst[A,B]`(a,b) \ a" proof - - assume "a : A" and "b : B" - then have "(a, b) : A \ B" .. + have "A : U" using assms(1) .. then show "fst[A,B]`(a,b) \ a" unfolding fst_nondep_def by simp qed -- cgit v1.2.3