From 120879c099a2fb71e67a41a1c852c5db65e9eb4f Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Mon, 28 May 2018 15:53:07 +0200 Subject: Dependent product rules done and proofs of typing properties so far work. Starting on dependent sums. --- HoTT.thy | 81 ++++++++++++++++++++++++++++++++++++++++++---------------------- 1 file changed, 54 insertions(+), 27 deletions(-) (limited to 'HoTT.thy') diff --git a/HoTT.thy b/HoTT.thy index a13b1d4..4713a0d 100644 --- a/HoTT.thy +++ b/HoTT.thy @@ -19,23 +19,38 @@ consts is_a_type :: "Term \ prop" ("(_ : U)" [0] 1000) is_of_type :: "[Term, Term] \ prop" ("(3_ :/ _)" [0, 0] 1000) -subsection \Basic axioms\ +subsection \Type families\ -subsubsection \Definitional equality\ +text "Type families are implemented as meta-level lambda terms of type \Term \ Term\ that further satisfy the following property." -text "We take the meta-equality \, defined by the Pure framework for any of its terms, and use it additionally for definitional/judgmental equality of types and terms in our theory. +abbreviation is_type_family :: "[(Term \ Term), Term] \ prop" ("(3_:/ _ \ U)") + where "P: A \ U \ (\x::Term. x : A \ P(x) : U)" -Note that the Pure framework already provides axioms and results for various properties of \, which we make use of and extend where necessary." +theorem constant_type_family: "\B : U; A : U\ \ \_. B: A \ U" + proof - + assume "B : U" + then show "\_. B: A \ U" . + qed -subsubsection \Type-related properties\ +subsection \Definitional equality\ -axiomatization where - equal_types: "\(A::Term) (B::Term) (x::Term). \A \ B; x : A\ \ x : B" and - inhabited_implies_type: "\(x::Term) (A::Term). x : A \ A : U" +text "We take the meta-equality \\\, defined by the Pure framework for any of its terms, and use it additionally for definitional/judgmental equality of types and terms in our theory. + +Note that the Pure framework already provides axioms and results for various properties of \\\, which we make use of and extend where necessary." + +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 + +lemmas type_equality [intro] = equal_types equal_types[rotated] equal_type_element equal_type_element[rotated] subsection \Basic types\ -subsubsection \Dependent product type\ +subsubsection \Dependent function/product\ consts Prod :: "[Term, (Term \ Term)] \ Term" @@ -43,36 +58,48 @@ syntax "_Prod" :: "[idt, Term, Term] \ Term" ("(3\_:_./ _)" 10) translations "\x:A. B" \ "CONST Prod A (\x. B)" -(* The above syntax translation binds the x in B *) +(* The above syntax translation binds the x in the expression B *) + +abbreviation Function :: "[Term, Term] \ Term" (infixr "\" 30) + where "A\B \ \_:A. B" axiomatization lambda :: "(Term \ Term) \ Term" (binder "\<^bold>\" 10) and appl :: "[Term, Term] \ Term" ("(3_`/_)" [10, 10] 60) where - Prod_form: "\(A::Term) (B::Term \ Term). \A : U; \(x::Term). x : A \ B(x) : U\ \ \x:A. B(x) : U" and - Prod_intro: "\(A::Term) (B::Term \ Term) (b::Term \ Term). \A : U; \(x::Term). x : A \ b(x) : B(x)\ \ \<^bold>\x. b(x) : \x:A. B(x)" and - Prod_elim: "\(A::Term) (B::Term \ Term) (f::Term) (a::Term). \f : \x:A. B(x); a : A\ \ f`a : B(a)" and - Prod_comp: "\(b::Term \ Term) (a::Term). (\<^bold>\x. b(x))`a \ b(a)" and - Prod_uniq: "\(A::Term) (B::Term \ Term) (f::Term). \f : \x:A. B(x)\ \ \<^bold>\x. (f`x) \ f" - -text "Observe that the metatype \Term \ Term\ is used to represent type families, for example \Prod\ takes a type \A\ and a type family \B\ and constructs a dependent function type from them." + Prod_form: "\(A::Term) (B::Term \ Term). \A : U; B : A \ U\ \ \x:A. B(x) : U" and + Prod_intro [intro]: "\(A::Term) (B::Term \ Term) (b::Term \ Term). \A : U; B : A \ U; \x::Term. x : A \ b(x) : B(x)\ \ \<^bold>\x. b(x) : \x:A. B(x)" and + Prod_elim [elim]: "\(A::Term) (B::Term \ Term) (f::Term) (a::Term). \f : \x:A. B(x); a : A\ \ f`a : B(a)" and + Prod_comp [simp]: "\(b::Term \ Term) (a::Term). (\<^bold>\x. b(x))`a \ b(a)" and + Prod_uniq [simp]: "\(A::Term) (B::Term \ Term) (f::Term). f : \x:A. B(x) \ \<^bold>\x. (f`x) \ f" 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)." -abbreviation Function :: "[Term, Term] \ Term" (infixr "\" 30) -where "A\B \ \_:A. B" +lemmas Prod_formation = Prod_form Prod_form[rotated] -subsubsection \Nondependent product type\ +subsubsection \Dependent pair/sum\ + +consts + Sum :: "[Term, Term \ Term] \ Term" +syntax + "_Sum" :: "[idt, Term, Term] \ Term" ("(3\_:_./ _)" 10) +translations + "\x:A. B" \ "CONST Sum A (\x. B)" + +abbreviation Pair :: "[Term, Term] \ Term" (infixr "\" 50) + where "A\B \ \_:A. B" axiomatization - Product :: "Term \ Term \ Term" ("(_\/ _)") and - pair :: "Term \ Term \ Term" ("(_,/ _)") and - rec_Product :: "Term \ Term \ Term \ Term \ Term" ("(rec'_Product'(_,_,_,_'))") + pair :: "[Term, Term] \ Term" ("(1'(_,/ _'))") and + indSum :: "[Term \ Term, Term \ Term, Term] \ Term" where - Product_form: "\A B. \A : U; B : U\ \ A\B : U" and - Product_intro: "\A B a b. \a : A; b : B\ \ (a,b) : A\B" and - Product_elim: "\A B C g. \A : U; B : U; C : U; g : A\B\C\ \ rec_Product(A,B,C,g) : (A\B)\C" and - Product_comp: "\A B C g a b. \C : U; g : A\B\C; a : A; b : B\ \ rec_Product(A,B,C,g)`(a,b) \ (g`a)`b" + Sum_form: "\(A::Term) (B::Term \ Term). \A : U; B: A \ U\ \ \x:A. B(x) : U" and + Sum_intro: "\(A::Term) (B::Term \ Term) (a::Term) (b::Term). \A : U; B: A \ U; a : A; b : B(a)\ \ (a, b) : \x:A. B(x)" and + Sum_elim: "\(A::Term) (B::Term \ Term) (C::Term \ Term) (f::Term \ Term) (p::Term). \A : U; B: A \ U; C: \x:A. B(x) \ U; \x y::Term. \x : A; y : B(x)\ \ f((x,y)) : C((x,y)); p : \x:A. B(x)\ \ (indSum C f p) : C(p)" + Sum_comp: "" + +text "A choice had to be made for the elimination rule: we formalize the function \f\ taking \a : A\ and \b : B(x)\ and returning \C((a,b))\ as a meta-lambda \f::Term \ Term\ instead of an object dependent function \f : \x:A. B(x)\. +However we should be able to later show the equivalence of the formalizations." \ \Projection onto first component\ (* -- cgit v1.2.3