From fc19fe90e7cb13acc03deaf061b2b6cf3df2d165 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Thu, 7 Jun 2018 19:35:32 +0200 Subject: Nondependent function arrow should bind tighter than the Pi former, but looser than equality. --- HoTT.thy | 64 +++++++++++++++++++++++++++++++++++++++++++--------------------- 1 file changed, 43 insertions(+), 21 deletions(-) (limited to 'HoTT.thy') diff --git a/HoTT.thy b/HoTT.thy index ee81ba4..c1c6e72 100644 --- a/HoTT.thy +++ b/HoTT.thy @@ -30,7 +30,7 @@ theorem equal_type_element: assumes "A \ B" and "x : A" shows "x : B" using assms by simp -lemmas type_equality [intro] = equal_types equal_types[rotated] equal_type_element equal_type_element[rotated] +lemmas type_equality [intro, simp] = equal_types equal_types[rotated] equal_type_element equal_type_element[rotated] section \Type families\ text "Type families are implemented using meta-level lambda expressions \P::Term \ Term\ that further satisfy the following property." @@ -46,14 +46,18 @@ axiomatization Prod :: "[Term, Term \ Term] \ Term" and lambda :: "[Term, Term \ Term] \ Term" syntax - "_PROD" :: "[idt, Term, Term] \ Term" ("(3\_:_./ _)" 30) - "_LAMBDA" :: "[idt, Term, Term] \ Term" ("(3\<^bold>\_:_./ _)" 30) + "_PROD" :: "[idt, Term, Term] \ Term" ("(3\_:_./ _)" 30) + "_LAMBDA" :: "[idt, Term, Term] \ Term" ("(3\<^bold>\_:_./ _)" 30) + "_PROD_ASCII" :: "[idt, Term, Term] \ Term" ("(3PROD _:_./ _)" 30) + "_LAMBDA_ASCII" :: "[idt, Term, Term] \ Term" ("(3%%_:_./ _)" 30) translations "\x:A. B" \ "CONST Prod A (\x. B)" "\<^bold>\x:A. b" \ "CONST lambda A (\x. b)" -(* The above syntax translations bind the x in the expressions B, b. *) + "PROD x:A. B" \ "CONST Prod A (\x. B)" + "%%x:A. b" \ "CONST lambda A (\x. b)" + (* The above syntax translations bind the x in the expressions B, b. *) -abbreviation Function :: "[Term, Term] \ Term" (infixr "\" 10) +abbreviation Function :: "[Term, Term] \ Term" (infixr "\" 80) where "A\B \ \_:A. B" axiomatization @@ -71,7 +75,7 @@ and and Prod_uniq [simp]: "\A f::Term. \<^bold>\x:A. (f`x) \ f" -lemmas Prod_formation = Prod_form Prod_form[rotated] +lemmas Prod_formation [intro] = Prod_form Prod_form[rotated] text "Note that the syntax \\<^bold>\\ (bold lambda) used for dependent functions clashes with the proof term syntax (cf. \
2.5.2 of the Isabelle/Isar Implementation)." @@ -80,11 +84,13 @@ subsection \Dependent pair/sum\ axiomatization Sum :: "[Term, Term \ Term] \ Term" syntax - "_Sum" :: "[idt, Term, Term] \ Term" ("(3\_:_./ _)" 20) + "_SUM" :: "[idt, Term, Term] \ Term" ("(3\_:_./ _)" 20) + "_SUM_ASCII" :: "[idt, Term, Term] \ Term" ("(3SUM _:_./ _)" 20) translations "\x:A. B" \ "CONST Sum A (\x. B)" + "SUM x:A. B" \ "CONST Sum A (\x. B)" -abbreviation Pair :: "[Term, Term] \ Term" (infixr "\" 50) +abbreviation Pair :: "[Term, Term] \ Term" (infixr "\" 50) where "A\B \ \_:A. B" axiomatization @@ -102,7 +108,7 @@ and and Sum_comp [simp]: "\(C::Term \ Term) (f::Term) (a::Term) (b::Term). indSum(C)`f`(a,b) \ f`a`b" -lemmas Sum_formation = Sum_form Sum_form[rotated] +lemmas Sum_formation [intro] = Sum_form Sum_form[rotated] text "We choose to formulate the elimination rule by using the object-level function type and function application as much as possible. Hence only the type family \C\ is left as a meta-level argument to the inductor indSum." @@ -145,35 +151,51 @@ subsection \Equality type\ axiomatization Equal :: "[Term, Term, Term] \ Term" syntax - "_EQUAL" :: "[Term, Term, Term] \ Term" ("(3_ =\<^sub>_/ _)") + "_EQUAL" :: "[Term, Term, Term] \ Term" ("(3_ =\<^sub>_/ _)" [101, 101] 100) + "_EQUAL_ASCII" :: "[Term, Term, Term] \ Term" ("(3_ =[_]/ _)" [101, 101] 100) translations "a =\<^sub>A b" \ "CONST Equal A a b" + "a =[A] b" \ "CONST Equal A a b" axiomatization refl :: "Term \ Term" and - indEqual :: "([Term, Term, Term] \ Term) \ Term" + indEqual :: "[Term, [Term, Term, Term] \ Term] \ Term" ("(indEqual[_])") where Equal_form: "\A a b::Term. \A : U; a : A; b : A\ \ a =\<^sub>A b : U" + (* Should I write a permuted version \\A : U; b : A; a : A\ \ \\? *) and Equal_intro [intro]: "\A x::Term. x : A \ refl(x) : x =\<^sub>A x" and Equal_elim [elim]: - "\(A::Term) (C::[Term, Term, Term] \ Term) (f::Term) (a::Term) (b::Term) (p::Term). \ - \x y p::Term. \x : A; y : A; p : x =\<^sub>A y\ \ C(x)(y)(p) : U; - f : \x:A. C(x)(x)(refl(x)); - a : A; - b : A; - p : a =\<^sub>A b\ \ indEqual(C)`f`a`b`p : C(a)(b)(p)" + "\(A::Term) (C::[Term, Term, Term] \ Term) (f::Term) (a::Term) (b::Term) (p::Term). + \ \x y::Term. \x : A; y : A\ \ C(x)(y): x =\<^sub>A y \ U; + f : \x:A. C(x)(x)(refl(x)); + a : A; + b : A; + p : a =\<^sub>A b \ + \ indEqual[A](C)`f`a`b`p : C(a)(b)(p)" and Equal_comp [simp]: - "\(C::[Term, Term, Term] \ Term) (f::Term) (a::Term). indEqual(C)`f`a`a`refl(a) \ f`a" + "\(A::Term) (C::[Term, Term, Term] \ Term) (f::Term) (a::Term). indEqual[A](C)`f`a`a`refl(a) \ f`a" + +lemmas Equal_formation [intro] = Equal_form Equal_form[rotated 1] Equal_form[rotated 2] subsubsection \Properties of equality\ -text "Inverse" +text "Symmetry/Path inverse" + +definition inv :: "[Term, Term, Term] \ Term" ("(1inv[_,/ _,/ _])") + where "inv[A,x,y] \ indEqual[A](\x y _. y =\<^sub>A x)`(\<^bold>\x:A. refl(x))`x`y" + +lemma inv_comp: "\A a::Term. a : A \ inv[A,a,a]`refl(a) \ refl(a)" unfolding inv_def by simp + +text "Transitivity/Path composition" + +definition compose' :: "Term \ Term" ("(1compose''[_])") + where "compose'[A] \ indEqual[A](\x y _. \z:A. \q: y =\<^sub>A z. x =\<^sub>A z)`(indEqual[A](\x z _. x =\<^sub>A z)`(\<^bold>\x:A. refl(x)))" + +lemma compose'_comp: "a : A \ compose'[A]`a`a`refl(a)`a`refl(a) \ refl(a)" unfolding compose'_def by simp -definition inv :: "Term \ Term" ("(_\<^sup>-\<^sup>1)") - where "inv \ " (* Tra la la.. *) end -- cgit v1.2.3