From d09095bec2c136f600edd0039a1cc1eae441d823 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 5 Jun 2018 18:42:54 +0200 Subject: Code formatting --- HoTT.thy | 95 ++++++++++++++++++++++++++++++++++++---------------------------- 1 file changed, 54 insertions(+), 41 deletions(-) (limited to 'HoTT.thy') diff --git a/HoTT.thy b/HoTT.thy index ef39734..ee81ba4 100644 --- a/HoTT.thy +++ b/HoTT.thy @@ -11,19 +11,13 @@ We do not implement universes, but simply follow the informal notation in the Ho typedecl Term -subsection \Judgments\ +section \Judgments\ consts is_a_type :: "Term \ prop" ("(_ : U)" [0] 1000) is_of_type :: "[Term, Term] \ prop" ("(3_ :/ _)" [0, 0] 1000) -subsection \Type families\ -text "Type families are implemented using meta-level lambda expressions \P::Term \ Term\ that further satisfy the following property." - -abbreviation is_type_family :: "[Term \ Term, Term] \ prop" ("(3_:/ _ \ U)") - where "P: A \ U \ (\x::Term. x : A \ P(x) : U)" - -subsection \Definitional equality\ +section \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. Note that the Pure framework already provides axioms and results for various properties of \\\, which we make use of and extend where necessary." @@ -38,9 +32,15 @@ theorem equal_type_element: lemmas type_equality [intro] = equal_types equal_types[rotated] equal_type_element equal_type_element[rotated] -subsection \Basic types\ +section \Type families\ +text "Type families are implemented using meta-level lambda expressions \P::Term \ Term\ that further satisfy the following property." -subsubsection \Dependent function/product\ +abbreviation is_type_family :: "[Term \ Term, Term] \ prop" ("(3_:/ _ \ U)") + where "P: A \ U \ (\x::Term. x : A \ P(x) : U)" + +section \Types\ + +subsection \Dependent function/product\ axiomatization Prod :: "[Term, Term \ Term] \ Term" and @@ -59,23 +59,23 @@ abbreviation Function :: "[Term, Term] \ Term" (infixr "\ 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) (a::Term). a : A \ (\<^bold>\x:A. b(x))`a \ b(a)" and - + 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) (a::Term). a : A \ (\<^bold>\x:A. b(x))`a \ b(a)" +and Prod_uniq [simp]: "\A 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\ +subsection \Dependent pair/sum\ axiomatization Sum :: "[Term, Term \ Term] \ Term" @@ -91,14 +91,15 @@ axiomatization pair :: "[Term, Term] \ Term" ("(1'(_,/ _'))") and indSum :: "(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 : A; b : B(a)\ \ (a, b) : \x:A. B(x)" and - - Sum_elim [elim]: "\(A::Term) (B::Term \ Term) (C::Term \ Term) (f::Term) (p::Term). - \C: \x:A. B(x) \ U; f : \x:A. \y:B(x). C((x,y)); p : \x:A. B(x)\ \ indSum(C)`f`p : C(p)" and - + 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 : A; b : B(a)\ \ (a, b) : \x:A. B(x)" +and + Sum_elim [elim]: + "\(A::Term) (B::Term \ Term) (C::Term \ Term) (f::Term) (p::Term). + \C: \x:A. B(x) \ U; f : \x:A. \y:B(x). C((x,y)); p : \x:A. B(x)\ \ indSum(C)`f`p : C(p)" +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] @@ -106,7 +107,7 @@ lemmas Sum_formation = 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." -text "Projection functions" +subsubsection \Projections\ consts fst :: "[Term, 'a] \ Term" ("(1fst[/_,/ _])") @@ -139,7 +140,7 @@ lemma snd_nondep_comp: "\a : A; b : B\ \ snd[A,B \ \Simplification rules for projections\ lemmas fst_snd_simps [simp] = fst_dep_comp snd_dep_comp fst_nondep_comp snd_nondep_comp -subsubsection \Equality type\ +subsection \Equality type\ axiomatization Equal :: "[Term, Term, Term] \ Term" @@ -152,16 +153,30 @@ axiomatization refl :: "Term \ Term" and indEqual :: "([Term, Term, Term] \ Term) \ Term" where - Equal_form: "\A a b::Term. \A : U; a : A; b : A\ \ a =\<^sub>A b : U" and - + Equal_form: "\A a b::Term. \A : U; a : A; b : A\ \ a =\<^sub>A b : U" +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)" +and + Equal_comp [simp]: + "\(C::[Term, Term, Term] \ Term) (f::Term) (a::Term). indEqual(C)`f`a`a`refl(a) \ f`a" -(* and - - Equal_elim [elim]: "\(C::[Term, Term, Term] \ Term) (f::Term) (x::Term) (y::Term) (p::Term). - \\ \ (indEqual C)`f`x`y`p : C(x)(y)(p)" +subsubsection \Properties of equality\ + +text "Inverse" + +definition inv :: "Term \ Term" ("(_\<^sup>-\<^sup>1)") + where "inv \ " (* Tra la la.. *) + +end -*) (* subsubsection \Empty type\ @@ -185,6 +200,4 @@ where Nat_intro2: "\n. n : Nat \ succ n : Nat" (* computation rules *) -*) - -end \ No newline at end of file +*) \ No newline at end of file -- cgit v1.2.3