diff options
Diffstat (limited to '')
| -rw-r--r-- | Coprod.thy | 8 | ||||
| -rw-r--r-- | Empty.thy | 4 | ||||
| -rw-r--r-- | Equal.thy | 10 | ||||
| -rw-r--r-- | EqualProps.thy | 75 | ||||
| -rw-r--r-- | HoTT_Base.thy | 99 | ||||
| -rw-r--r-- | HoTT_Methods.thy | 6 | ||||
| -rw-r--r-- | Nat.thy | 8 | ||||
| -rw-r--r-- | Prod.thy | 18 | ||||
| -rw-r--r-- | Sum.thy | 12 | ||||
| -rw-r--r-- | Univalence.thy | 37 | ||||
| -rw-r--r-- | tests/Test.thy | 2 |
11 files changed, 162 insertions, 117 deletions
@@ -12,10 +12,10 @@ begin section \<open>Constants and type rules\<close> axiomatization - Coprod :: "[Term, Term] \<Rightarrow> Term" (infixr "+" 50) and - inl :: "Term \<Rightarrow> Term" and - inr :: "Term \<Rightarrow> Term" and - indCoprod :: "[Term \<Rightarrow> Term, Term \<Rightarrow> Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>+)") + Coprod :: "[t, t] \<Rightarrow> t" (infixr "+" 50) and + inl :: "t \<Rightarrow> t" and + inr :: "t \<Rightarrow> t" and + indCoprod :: "[t \<Rightarrow> t, t \<Rightarrow> t, t] \<Rightarrow> t" ("(1ind\<^sub>+)") where Coprod_form: "\<lbrakk>A: U i; B: U i\<rbrakk> \<Longrightarrow> A + B: U i" and @@ -14,8 +14,8 @@ section \<open>Constants and type rules\<close> section \<open>Empty type\<close> axiomatization - Empty :: Term ("\<zero>") and - indEmpty :: "Term \<Rightarrow> Term" ("(1ind\<^sub>\<zero>)") + Empty :: t ("\<zero>") and + indEmpty :: "t \<Rightarrow> t" ("(1ind\<^sub>\<zero>)") where Empty_form: "\<zero>: U O" and @@ -12,13 +12,13 @@ begin section \<open>Constants and syntax\<close> axiomatization - Equal :: "[Term, Term, Term] \<Rightarrow> Term" and - refl :: "Term \<Rightarrow> Term" and - indEqual :: "[Term \<Rightarrow> Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>=)") + Equal :: "[t, t, t] \<Rightarrow> t" and + refl :: "t \<Rightarrow> t" and + indEqual :: "[t \<Rightarrow> t, t] \<Rightarrow> t" ("(1ind\<^sub>=)") syntax - "_EQUAL" :: "[Term, Term, Term] \<Rightarrow> Term" ("(3_ =\<^sub>_/ _)" [101, 0, 101] 100) - "_EQUAL_ASCII" :: "[Term, Term, Term] \<Rightarrow> Term" ("(3_ =[_]/ _)" [101, 0, 101] 100) + "_EQUAL" :: "[t, t, t] \<Rightarrow> t" ("(3_ =\<^sub>_/ _)" [101, 0, 101] 100) + "_EQUAL_ASCII" :: "[t, t, t] \<Rightarrow> t" ("(3_ =[_]/ _)" [101, 0, 101] 100) translations "a =[A] b" \<rightleftharpoons> "CONST Equal A a b" "a =\<^sub>A b" \<rightharpoonup> "CONST Equal A a b" diff --git a/EqualProps.thy b/EqualProps.thy index 5db8487..19c788c 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -14,7 +14,7 @@ begin section \<open>Symmetry / Path inverse\<close> -definition inv :: "Term \<Rightarrow> Term" ("_\<inverse>" [1000] 1000) where "p\<inverse> \<equiv> ind\<^sub>= (\<lambda>x. (refl x)) p" +definition inv :: "t \<Rightarrow> t" ("_\<inverse>" [1000] 1000) where "p\<inverse> \<equiv> ind\<^sub>= (\<lambda>x. (refl x)) p" text " In the proof below we begin by using path induction on \<open>p\<close> with the application of \<open>rule Equal_elim\<close>, telling Isabelle the specific substitutions to use. @@ -46,7 +46,7 @@ text " Raw composition function, of type \<open>\<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)\<close> polymorphic over the type \<open>A\<close>. " -definition rpathcomp :: Term where "rpathcomp \<equiv> \<^bold>\<lambda>_ _ p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>_ q. ind\<^sub>= (\<lambda>x. (refl x)) q) p" +definition rpathcomp :: t where "rpathcomp \<equiv> \<^bold>\<lambda>_ _ p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>_ q. ind\<^sub>= (\<lambda>x. (refl x)) q) p" text " More complicated proofs---the nested path inductions require more explicit step-by-step rule applications: @@ -194,7 +194,7 @@ qed fact text "The raw object lambda term is cumbersome to use, so we define a simpler constant instead." -axiomatization pathcomp :: "[Term, Term] \<Rightarrow> Term" (infixl "\<bullet>" 120) where +axiomatization pathcomp :: "[t, t] \<Rightarrow> t" (infixl "\<bullet>" 120) where pathcomp_def: "\<lbrakk> A: U i; x: A; y: A; z: A; @@ -216,9 +216,72 @@ lemma pathcomp_comp: by (subst pathcomp_def) (routine lems: assms rpathcomp_comp) -lemmas EqualProps_type [intro] = inv_type pathcomp_type -lemmas EqualProps_comp [comp] = inv_comp pathcomp_comp +lemmas inv_type [intro] +lemmas pathcomp_type [intro] +lemmas inv_comp [comp] +lemmas pathcomp_comp [comp] + + +section \<open>Weak higher groupoid structure of types\<close> + +schematic_goal whg1a: + assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" + shows "?a: p =[x =\<^sub>A y] (p \<bullet> (refl(y)))" +proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) + show "\<And>x. x: A \<Longrightarrow> refl(refl(x)): refl(x) =[x =\<^sub>A x] (refl(x) \<bullet> refl(x))" + by compute (routine lems: assms) +qed (routine lems: assms) + +schematic_goal whg1b: + assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" + shows "?a: p =[x =\<^sub>A y] (refl(x) \<bullet> p)" +proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) + show "\<And>x. x: A \<Longrightarrow> refl(refl(x)): refl(x) =[x =\<^sub>A x] (refl(x) \<bullet> refl(x))" + by compute (routine lems: assms) +qed (routine lems: assms) + +schematic_goal whg2a: + assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" + shows "?a: (p\<inverse> \<bullet> p) =[y =\<^sub>A y] refl(y)" +proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) + show "\<And>x. x: A \<Longrightarrow> refl(refl(x)): ((refl(x))\<inverse> \<bullet> refl(x)) =[x =\<^sub>A x] refl(x)" + by (compute | routine lems: assms)+ +qed (routine lems: assms)+ + +schematic_goal whg2b: + assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" + shows "?a: (p \<bullet> p\<inverse>) =[x =\<^sub>A x] refl(x)" +proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) + show "\<And>x. x: A \<Longrightarrow> refl(refl(x)): (refl(x) \<bullet> (refl(x))\<inverse>) =[x =\<^sub>A x] refl(x)" + by (compute | routine lems: assms)+ +qed (routine lems: assms)+ + +schematic_goal whg3: + assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" + shows "?a: p\<inverse>\<inverse> =[x =\<^sub>A y] p" +proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) + show "\<And>x. x: A \<Longrightarrow> refl(refl(x)): (refl(x))\<inverse>\<inverse> =[x =\<^sub>A x] refl(x)" + by (compute | routine lems: assms)+ +qed (routine lems: assms) + + +lemma assumes "A: U(i)" shows "\<And>x. x: A \<Longrightarrow> refl(x): x =\<^sub>A x" +by (rule Prod_atomize[where ?A=A and ?B="\<lambda>x. x =\<^sub>A x"]) (routine lems: assms) + + +schematic_goal + assumes + "A: U(i)" and + "x: A" "y: A" "z: A" "w: A" and + "p: x =\<^sub>A y" "q: y =\<^sub>A z" "r: z =\<^sub>A w" + shows + "?a: p \<bullet> (q \<bullet> r) =[x =\<^sub>A w] (p \<bullet> q) \<bullet> r" +proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) + fix y assume "y: A" + show "refl(q \<bullet> r): refl(y) \<bullet> (q \<bullet> r) =[y =\<^sub>A w] (refl(y) \<bullet> q) \<bullet> r" + proof (compute lems: whg1b) + section \<open>Higher groupoid structure of types\<close> @@ -275,7 +338,7 @@ sorry section \<open>Transport\<close> -definition transport :: "Term \<Rightarrow> Term" where +definition transport :: "t \<Rightarrow> t" where "transport p \<equiv> ind\<^sub>= (\<lambda>x. (\<^bold>\<lambda>x. x)) p" text "Note that \<open>transport\<close> is a polymorphic function in our formulation." diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 916f6aa..07fbfc4 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -1,94 +1,77 @@ (* Title: HoTT/HoTT_Base.thy - Author: Josh Chen + Author: Joshua Chen -Basic setup and definitions of a homotopy type theory object logic with a cumulative universe hierarchy à la Russell. +Basic setup of a homotopy type theory object logic with a Russell-style cumulative universe hierarchy. *) theory HoTT_Base - imports Pure +imports + Pure + "HOL-Eisbach.Eisbach" + begin -section \<open>Foundational definitions\<close> +section \<open>Basic setup\<close> -text "Meta syntactic type for object-logic types and terms." +typedecl t \<comment> \<open>Type of object types and terms\<close> +typedecl ord \<comment> \<open>Type of meta-level numerals\<close> -typedecl Term +axiomatization + O :: ord and + Suc :: "ord \<Rightarrow> ord" and + lt :: "[ord, ord] \<Rightarrow> prop" (infix "<" 999) +where + lt_Suc [intro]: "n < (Suc n)" and + lt_trans [intro]: "\<lbrakk>m1 < m2; m2 < m3\<rbrakk> \<Longrightarrow> m1 < m3" and + Suc_monotone [simp]: "m < n \<Longrightarrow> (Suc m) < (Suc n)" +method proveSuc = (rule lt_Suc | (rule lt_trans, (rule lt_Suc)+)+) -text " - Formalize the typing judgment \<open>a: A\<close>. - For judgmental/definitional equality we use the existing Pure equality \<open>\<equiv>\<close> and hence do not need to define a separate judgment for it. -" +text \<open>Method @{method proveSuc} proves statements of the form \<open>n < (Suc (... (Suc n) ...))\<close>.\<close> -judgment has_type :: "[Term, Term] \<Rightarrow> prop" ("(3_:/ _)" [0, 0] 1000) +section \<open>Judgment\<close> -section \<open>Universe hierarchy\<close> +judgment hastype :: "[t, t] \<Rightarrow> prop" ("(3_:/ _)") -text "Finite meta-ordinals to index the universes." -typedecl Ord +section \<open>Universes\<close> axiomatization - O :: Ord and - S :: "Ord \<Rightarrow> Ord" ("S _" [0] 1000) and - lt :: "[Ord, Ord] \<Rightarrow> prop" (infix "<" 999) and - leq :: "[Ord, Ord] \<Rightarrow> prop" (infix "\<le>" 999) + U :: "ord \<Rightarrow> t" where - lt_min: "\<And>n. O < S n" -and - lt_monotone1: "\<And>n. n < S n" -and - lt_monotone2: "\<And>m n. m < n \<Longrightarrow> S m < S n" -and - leq_min: "\<And>n. O \<le> n" -and - leq_monotone1: "\<And>n. n \<le> S n" -and - leq_monotone2: "\<And>m n. m \<le> n \<Longrightarrow> S m \<le> S n" - -lemmas Ord_rules [intro] = lt_min lt_monotone1 lt_monotone2 leq_min leq_monotone1 leq_monotone2 - \<comment> \<open>Enables \<open>standard\<close> to automatically solve inequalities.\<close> - -text "Define the universe types." + U_hierarchy: "i < j \<Longrightarrow> U i: U j" and + U_cumulative: "\<lbrakk>A: U i; i < j\<rbrakk> \<Longrightarrow> A: U j" -axiomatization - U :: "Ord \<Rightarrow> Term" -where - U_hierarchy: "\<And>i j. i < j \<Longrightarrow> U i: U j" -and - U_cumulative: "\<And>A i j. \<lbrakk>A: U i; i \<le> j\<rbrakk> \<Longrightarrow> A: U j" +text \<open> +Using method @{method rule} with @{thm U_cumulative} is unsafe, if applied blindly it will typically lead to non-termination. +One should instead use @{method elim}, or instantiate @{thm U_cumulative} suitably. +\<close> -text " - The rule \<open>U_cumulative\<close> is very unsafe: if used as-is it will usually lead to an infinite rewrite loop! - To avoid this, it should be instantiated before being applied. -" +method cumulativity = (elim U_cumulative, proveSuc) \<comment> \<open>Proves \<open>A: U i \<Longrightarrow> A: U (Suc (... (Suc i) ...))\<close>.\<close> +method hierarchy = (rule U_hierarchy, proveSuc) \<comment> \<open>Proves \<open>U i: U (Suc (... (Suc i) ...)).\<close>\<close> section \<open>Type families\<close> -text " - The following abbreviation constrains the output type of a meta lambda expression when given input of certain type. -" - -abbreviation (input) constrained :: "[Term \<Rightarrow> Term, Term, Term] \<Rightarrow> prop" ("(1_: _ \<longrightarrow> _)") +abbreviation (input) constrained :: "[t \<Rightarrow> t, t, t] \<Rightarrow> prop" ("(1_:/ _ \<longrightarrow> _)") where "f: A \<longrightarrow> B \<equiv> (\<And>x. x : A \<Longrightarrow> f x: B)" -text " - The above is used to define type families, which are constrained meta-lambdas \<open>P: A \<longrightarrow> B\<close> where \<open>A\<close> and \<open>B\<close> are small types. -" +text \<open> +The abbreviation @{abbrev constrained} is used to define type families, which are constrained expressions @{term "P: A \<longrightarrow> B"} where @{term "A::t"} and @{term "B::t"} are small types. +\<close> -type_synonym Typefam = "Term \<Rightarrow> Term" +type_synonym tf = "t \<Rightarrow> t" \<comment> \<open>Type of type families.\<close> section \<open>Named theorems\<close> -text " - Named theorems to be used by proof methods later (see HoTT_Methods.thy). - - \<open>wellform\<close> declares necessary wellformedness conditions for type and inhabitation judgments, while \<open>comp\<close> declares computation rules, which are usually passed to invocations of the method \<open>subst\<close> to perform equational rewriting. -" +text \<open> +Declare named theorems to be used by proof methods defined in @{file HoTT_Methods.thy}. +\<open>wellform\<close> declares necessary well-formedness conditions for type and inhabitation judgments. +\<open>comp\<close> declares computation rules, which are usually passed to invocations of the method \<open>subst\<close> to perform equational rewriting. +\<close> named_theorems wellform named_theorems comp diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index 32e412b..abb6dda 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -14,12 +14,12 @@ begin section \<open>Deriving typing judgments\<close> +method routine uses lems = (assumption | rule lems | standard)+ + text " - \<open>routine\<close> proves routine type judgments \<open>a : A\<close> using the rules declared [intro] in the respective theory files, as well as additional provided lemmas. + @{method routine} proves routine type judgments \<open>a : A\<close> using the rules declared [intro] in the respective theory files, as well as additional provided lemmas. " -method routine uses lems = (assumption | rule lems | standard)+ - text " \<open>wellformed'\<close> finds a proof of any valid typing judgment derivable from the judgment passed as \<open>jdmt\<close>. If no judgment is passed, it will try to resolve with the theorems declared \<open>wellform\<close>. @@ -12,10 +12,10 @@ begin section \<open>Constants and type rules\<close> axiomatization - Nat :: Term ("\<nat>") and - zero :: Term ("0") and - succ :: "Term \<Rightarrow> Term" and - indNat :: "[[Term, Term] \<Rightarrow> Term, Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>\<nat>)") + Nat :: t ("\<nat>") and + zero :: t ("0") and + succ :: "t \<Rightarrow> t" and + indNat :: "[[t, t] \<Rightarrow> t, t, t] \<Rightarrow> t" ("(1ind\<^sub>\<nat>)") where Nat_form: "\<nat>: U O" and @@ -12,14 +12,14 @@ begin section \<open>Constants and syntax\<close> axiomatization - Prod :: "[Term, Typefam] \<Rightarrow> Term" and - lambda :: "(Term \<Rightarrow> Term) \<Rightarrow> Term" (binder "\<^bold>\<lambda>" 30) and - appl :: "[Term, Term] \<Rightarrow> Term" (infixl "`" 60) + Prod :: "[t, tf] \<Rightarrow> t" and + lambda :: "(t \<Rightarrow> t) \<Rightarrow> t" (binder "\<^bold>\<lambda>" 30) and + appl :: "[t, t] \<Rightarrow> t" (infixl "`" 60) \<comment> \<open>Application binds tighter than abstraction.\<close> syntax - "_PROD" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3\<Prod>_:_./ _)" 30) - "_PROD_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3PROD _:_./ _)" 30) + "_PROD" :: "[idt, t, t] \<Rightarrow> t" ("(3\<Prod>_:_./ _)" 30) + "_PROD_ASCII" :: "[idt, t, t] \<Rightarrow> t" ("(3PROD _:_./ _)" 30) text "The translations below bind the variable \<open>x\<close> in the expressions \<open>B\<close> and \<open>b\<close>." @@ -29,7 +29,7 @@ translations text "Nondependent functions are a special case." -abbreviation Function :: "[Term, Term] \<Rightarrow> Term" (infixr "\<rightarrow>" 40) +abbreviation Function :: "[t, t] \<Rightarrow> t" (infixr "\<rightarrow>" 40) where "A \<rightarrow> B \<equiv> \<Prod>_: A. B" @@ -75,15 +75,15 @@ lemmas Prod_routine [intro] = Prod_form Prod_intro Prod_elim section \<open>Function composition\<close> -definition compose :: "[Term, Term] \<Rightarrow> Term" (infixr "o" 110) where "g o f \<equiv> \<^bold>\<lambda>x. g`(f`x)" +definition compose :: "[t, t] \<Rightarrow> t" (infixr "o" 110) where "g o f \<equiv> \<^bold>\<lambda>x. g`(f`x)" -syntax "_COMPOSE" :: "[Term, Term] \<Rightarrow> Term" (infixr "\<circ>" 110) +syntax "_COMPOSE" :: "[t, t] \<Rightarrow> t" (infixr "\<circ>" 110) translations "g \<circ> f" \<rightleftharpoons> "g o f" section \<open>Polymorphic identity function\<close> -abbreviation id :: Term where "id \<equiv> \<^bold>\<lambda>x. x" +abbreviation id :: t where "id \<equiv> \<^bold>\<lambda>x. x" end @@ -12,13 +12,13 @@ begin section \<open>Constants and syntax\<close> axiomatization - Sum :: "[Term, Typefam] \<Rightarrow> Term" and - pair :: "[Term, Term] \<Rightarrow> Term" ("(1<_,/ _>)") and - indSum :: "[[Term, Term] \<Rightarrow> Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>\<Sum>)") + Sum :: "[t, Typefam] \<Rightarrow> t" and + pair :: "[t, t] \<Rightarrow> t" ("(1<_,/ _>)") and + indSum :: "[[t, t] \<Rightarrow> t, t] \<Rightarrow> t" ("(1ind\<^sub>\<Sum>)") syntax - "_SUM" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3\<Sum>_:_./ _)" 20) - "_SUM_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3SUM _:_./ _)" 20) + "_SUM" :: "[idt, t, t] \<Rightarrow> t" ("(3\<Sum>_:_./ _)" 20) + "_SUM_ASCII" :: "[idt, t, t] \<Rightarrow> t" ("(3SUM _:_./ _)" 20) translations "\<Sum>x:A. B" \<rightleftharpoons> "CONST Sum A (\<lambda>x. B)" @@ -26,7 +26,7 @@ translations text "Nondependent pair." -abbreviation Pair :: "[Term, Term] \<Rightarrow> Term" (infixr "\<times>" 50) +abbreviation Pair :: "[t, t] \<Rightarrow> t" (infixr "\<times>" 50) where "A \<times> B \<equiv> \<Sum>_:A. B" diff --git a/Univalence.thy b/Univalence.thy index b7f4400..001ee33 100644 --- a/Univalence.thy +++ b/Univalence.thy @@ -1,32 +1,31 @@ (* Title: HoTT/Univalence.thy - Author: Josh Chen + Author: Joshua Chen Definitions of homotopy, equivalence and the univalence axiom. *) theory Univalence - imports - HoTT_Methods - EqualProps - ProdProps - Sum +imports + HoTT_Methods + EqualProps + ProdProps + Sum + begin section \<open>Homotopy and equivalence\<close> -text "We define polymorphic constants implementing the definitions of homotopy and equivalence." - -axiomatization homotopic :: "[Term, Term] \<Rightarrow> Term" (infix "~" 100) where +axiomatization homotopic :: "[t, t] \<Rightarrow> t" (infix "~" 100) where homotopic_def: "\<lbrakk> f: \<Prod>x:A. B x; g: \<Prod>x:A. B x \<rbrakk> \<Longrightarrow> f ~ g \<equiv> \<Prod>x:A. (f`x) =[B x] (g`x)" -axiomatization isequiv :: "Term \<Rightarrow> Term" where +axiomatization isequiv :: "t \<Rightarrow> t" where isequiv_def: "f: A \<rightarrow> B \<Longrightarrow> isequiv f \<equiv> (\<Sum>g: B \<rightarrow> A. g \<circ> f ~ id) \<times> (\<Sum>g: B \<rightarrow> A. f \<circ> g ~ id)" -definition equivalence :: "[Term, Term] \<Rightarrow> Term" (infix "\<simeq>" 100) +definition equivalence :: "[t, t] \<Rightarrow> t" (infix "\<simeq>" 100) where "A \<simeq> B \<equiv> \<Sum>f: A \<rightarrow> B. isequiv f" @@ -75,7 +74,7 @@ qed (rule assms) section \<open>idtoeqv and the univalence axiom\<close> -definition idtoeqv :: Term +definition idtoeqv :: t where "idtoeqv \<equiv> \<^bold>\<lambda>p. <transport p, ind\<^sub>= (\<lambda>A. <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>) p>" @@ -94,9 +93,9 @@ proof } show "transport p: A \<rightarrow> B" - proof (rule transport_type[where ?P="\<lambda>x. x" and ?A="U i" and ?i="S i"]) - show "\<And>x. x: U i \<Longrightarrow> x: U S i" by (elim U_cumulative) standard - show "U i: U S i" by (rule U_hierarchy) standard + proof (rule transport_type[where ?P="\<lambda>x. x" and ?A="U i" and ?i="Suc i"]) + show "\<And>x. x: U i \<Longrightarrow> x: U (Suc i)" by cumulativity + show "U i: U (Suc i)" by hierarchy qed fact+ show "ind\<^sub>= (\<lambda>A. <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>) p: isequiv (transport p)" @@ -112,8 +111,8 @@ proof (\<Sum>g:A \<rightarrow> A. g \<circ> (transport (refl A)) ~ id) \<times> (\<Sum>g:A \<rightarrow> A. (transport (refl A)) \<circ> g ~ id)" proof (subst (1 2) transport_comp) - show "U i: U S i" by (rule U_hierarchy) standard - show "U i: U S i" by (rule U_hierarchy) standard + show "U i: U (Suc i)" by (rule U_hierarchy) rule + show "U i: U (Suc i)" by (rule U_hierarchy) rule show "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: (\<Sum>g:A \<rightarrow> A. g \<circ> id ~ id) \<times> (\<Sum>g:A \<rightarrow> A. id \<circ> g ~ id)" @@ -164,13 +163,13 @@ proof qed next - show "A =[U i] B: U (S i)" by (derive lems: assms | rule U_hierarchy)+ + show "A =[U i] B: U (Suc i)" proof (derive lems: assms, (rule U_hierarchy, rule lt_Suc)?)+ qed text "The univalence axiom." -axiomatization univalence :: Term where +axiomatization univalence :: t where UA: "univalence: isequiv idtoeqv" diff --git a/tests/Test.thy b/tests/Test.thy index b0eb87a..de65dbd 100644 --- a/tests/Test.thy +++ b/tests/Test.thy @@ -23,7 +23,7 @@ declare[[unify_trace_simp, unify_trace_types, simp_trace, simp_trace_depth_limit \<comment> \<open>Turn on trace for unification and the simplifier, for debugging.\<close> -section \<open>\<Pi>-type\<close> +section \<open>\<Prod>-type\<close> subsection \<open>Typing functions\<close> |