From 095bc4a60ab2c38a56c34b4b99d363c4c0f14e3d Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Wed, 30 May 2018 15:39:35 +0200 Subject: New type rules for dependent product and sum. --- HoTT.thy | 41 +++++++++++++++++++++++++++++------------ 1 file changed, 29 insertions(+), 12 deletions(-) (limited to 'HoTT.thy') diff --git a/HoTT.thy b/HoTT.thy index cf21304..6de4efb 100644 --- a/HoTT.thy +++ b/HoTT.thy @@ -26,12 +26,17 @@ text "Type families are implemented as meta-level lambda terms of type \Te abbreviation is_type_family :: "[(Term \ Term), Term] \ prop" ("(3_:/ _ \ U)") where "P: A \ U \ (\x::Term. x : A \ P(x) : U)" -theorem constant_type_family: "\B : U; A : U\ \ \_. B: A \ U" +\ \ +I originally wrote the following, but I'm not sure it's useful. +\theorem constant_type_family': "B : U \ \_. B: A \ U" proof - assume "B : U" then show "\_. B: A \ U" . qed +lemmas constant_type_family = constant_type_family' constant_type_family'[rotated]\ +\ + subsection \Definitional equality\ 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. @@ -70,15 +75,21 @@ axiomatization appl :: "[Term, Term] \ Term" (infixl "`" 60) where 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). (\x::Term. x : A \ b(x) : B(x)) \ \<^bold>\x:A. 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]: "\(A::Term) (B::Term \ Term) (b::Term \ Term) (a::Term). \\x::Term. x : A \ b(x) : B(x); a : A\ \ (\<^bold>\x:A. b(x))`a \ b(a)" and - Prod_uniq [simp]: "\(A::Term) (B::Term \ Term) (f::Term). f : \x:A. B(x) \ \<^bold>\x:A. (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)." + Prod_intro [intro]: "\(A::Term) (b::Term \ Term) (B::Term \ Term). + (\x::Term. x : A \ b(x) : B(x)) \ \<^bold>\x:A. b(x) : \x:A. B(x)" and + + Prod_elim [elim]: "\(f::Term) (A::Term) (B::Term \ Term) (a::Term). + \f : \x:A. B(x); a : A\ \ f`a : B(a)" and + + Prod_comp [simp]: "\(a::Term) (A::Term) (b::Term \ Term). a : A \ (\<^bold>\x:A. b(x))`a \ b(a)" and + + Prod_uniq [simp]: "\(A::Term) (f::Term). \<^bold>\x:A. (f`x) \ f" lemmas Prod_formation = 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)." + subsubsection \Dependent pair/sum\ consts @@ -96,14 +107,20 @@ axiomatization indSum :: "[Term \ Term, Term \ Term, Term] \ Term" where Sum_form: "\(A::Term) (B::Term \ Term). \A : U; B: A \ U\ \ \x:A. B(x) : U" and - Sum_intro [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 [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)" and - Sum_comp [simp]: "\(A::Term) (B::Term \ Term) (C::Term \ Term) (f::Term \ Term) (a::Term) (b::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)); a : A; b : B(a)\ \ (indSum C f (a,b)) \ f((a,b))" -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 level \f::Term \ Term\ instead of an object logic dependent function \f : \x:A. B(x)\. -However we should be able to later show the equivalence of the formalizations." + Sum_intro [intro]: "\(A::Term) (B::Term \ Term) (a::Term) (b::Term). + \a : A; b : B(a)\ \ (a, b) : \x:A. B(x)" and + + Sum_elim [elim]: "\(A::Term) (B::Term \ Term) (C::Term \ Term) (f::Term \ Term) (p::Term). + \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)" and + Sum_comp [simp]: "\(A::Term) (B::Term \ Term) (C::Term \ Term) (f::Term \ Term) (a::Term) (b::Term). + (indSum C f (a,b)) \ f((a,b))" +lemmas Sum_formation = Sum_form Sum_form[rotated] + +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 level \f::Term \ Term\ instead of an object logic dependent function \f : \x:A. B(x)\. +However we should be able to later show the equivalence of the formalizations." \ \Projection onto first component\ (* @@ -125,7 +142,7 @@ subsubsection \Natural numbers\ axiomatization Nat :: Term and zero :: Term ("0") and - succ :: "Term \ Term" and (* how to enforce \succ : Nat\Nat\? *) + succ :: "Term \ Term" and (* how to enforce \succ : Nat\Nat\? *) ind_Nat :: "Term \ Term \ Term \ Term \ Term" where Nat_form: "Nat : U" and -- cgit v1.2.3