diff options
Diffstat (limited to '')
| -rw-r--r-- | Coprod.thy | 64 | ||||
| -rw-r--r-- | Empty.thy | 22 | ||||
| -rw-r--r-- | HoTT.thy | 2 | ||||
| -rw-r--r-- | HoTT_Base.thy | 25 | ||||
| -rw-r--r-- | HoTT_Methods.thy | 56 | ||||
| -rw-r--r-- | Nat.thy | 60 | ||||
| -rw-r--r-- | Proj.thy | 56 | ||||
| -rw-r--r-- | Sum.thy | 57 | ||||
| -rw-r--r-- | Unit.thy | 32 |
9 files changed, 155 insertions, 219 deletions
@@ -1,65 +1,49 @@ -(* Title: HoTT/Coprod.thy - Author: Josh Chen +(* +Title: Coprod.thy +Author: Joshua Chen +Date: 2018 Coproduct type *) theory Coprod - imports HoTT_Base -begin +imports HoTT_Base +begin -section \<open>Constants and type rules\<close> axiomatization - Coprod :: "[t, t] \<Rightarrow> t" (infixr "+" 50) and - inl :: "t \<Rightarrow> t" and - inr :: "t \<Rightarrow> t" and + 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 - Coprod_intro_inl: "\<lbrakk>a: A; B: U i\<rbrakk> \<Longrightarrow> inl a: A + B" -and - Coprod_intro_inr: "\<lbrakk>b: B; A: U i\<rbrakk> \<Longrightarrow> inr b: A + B" -and + Coprod_form: "\<lbrakk>A: U i; B: U i\<rbrakk> \<Longrightarrow> A + B: U i" and + + Coprod_intro_inl: "\<lbrakk>a: A; B: U i\<rbrakk> \<Longrightarrow> inl a: A + B" and + + Coprod_intro_inr: "\<lbrakk>b: B; A: U i\<rbrakk> \<Longrightarrow> inr b: A + B" and + Coprod_elim: "\<lbrakk> + u: A + B; C: A + B \<longrightarrow> U i; \<And>x. x: A \<Longrightarrow> c x: C (inl x); - \<And>y. y: B \<Longrightarrow> d y: C (inr y); - u: A + B - \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d u: C u" -and + \<And>y. y: B \<Longrightarrow> d y: C (inr y) \<rbrakk> \<Longrightarrow> ind\<^sub>+ (\<lambda> x. c x) (\<lambda>y. d y) u: C u" and + Coprod_comp_inl: "\<lbrakk> + a: A; C: A + B \<longrightarrow> U i; \<And>x. x: A \<Longrightarrow> c x: C (inl x); - \<And>y. y: B \<Longrightarrow> d y: C (inr y); - a: A - \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d (inl a) \<equiv> c a" -and + \<And>y. y: B \<Longrightarrow> d y: C (inr y) \<rbrakk> \<Longrightarrow> ind\<^sub>+ (\<lambda>x. c x) (\<lambda>y. d y) (inl a) \<equiv> c a" and + Coprod_comp_inr: "\<lbrakk> + b: B; C: A + B \<longrightarrow> U i; \<And>x. x: A \<Longrightarrow> c x: C (inl x); - \<And>y. y: B \<Longrightarrow> d y: C (inr y); - b: B - \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d (inr b) \<equiv> d b" - - -text "Admissible formation inference rules:" - -axiomatization where - Coprod_wellform1: "A + B: U i \<Longrightarrow> A: U i" -and - Coprod_wellform2: "A + B: U i \<Longrightarrow> B: U i" - - -text "Rule attribute declarations:" - -lemmas Coprod_intro = Coprod_intro_inl Coprod_intro_inr + \<And>y. y: B \<Longrightarrow> d y: C (inr y) \<rbrakk> \<Longrightarrow> ind\<^sub>+ (\<lambda>x. c x) (\<lambda>y. d y) (inr b) \<equiv> d b" +lemmas Coprod_routine [intro] = Coprod_form Coprod_intro_inl Coprod_intro_inr Coprod_elim lemmas Coprod_comp [comp] = Coprod_comp_inl Coprod_comp_inr -lemmas Coprod_wellform [wellform] = Coprod_wellform1 Coprod_wellform2 -lemmas Coprod_routine [intro] = Coprod_form Coprod_intro Coprod_elim end @@ -1,28 +1,24 @@ -(* Title: HoTT/Empty.thy - Author: Josh Chen +(* +Title: Empty.thy +Author: Joshua Chen +Date: 2018 Empty type *) theory Empty - imports HoTT_Base -begin - +imports HoTT_Base -section \<open>Constants and type rules\<close> +begin -section \<open>Empty type\<close> axiomatization - Empty :: t ("\<zero>") and + Empty :: t ("\<zero>") and indEmpty :: "t \<Rightarrow> t" ("(1ind\<^sub>\<zero>)") where - Empty_form: "\<zero>: U O" -and - Empty_elim: "\<lbrakk>C: \<zero> \<longrightarrow> U i; z: \<zero>\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero> z: C z" - + Empty_form: "\<zero>: U O" and -text "Rule attribute declarations:" + Empty_elim: "\<lbrakk>a: \<zero>; C: \<zero> \<longrightarrow> U i\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero> a: C a" lemmas Empty_routine [intro] = Empty_form Empty_elim @@ -30,7 +30,7 @@ begin lemmas forms = Nat_form Prod_form Sum_form Coprod_form Equal_form Unit_form Empty_form lemmas intros = - Nat_intro Prod_intro Sum_intro Equal_intro Coprod_intro Unit_intro + Nat_intro_0 Nat_intro_succ Prod_intro Sum_intro Equal_intro Coprod_intro_inl Coprod_intro_inr Unit_intro lemmas elims = Nat_elim Prod_elim Sum_elim Equal_elim Coprod_elim Unit_elim Empty_elim lemmas routines = diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 07fbfc4..efc6182 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -1,7 +1,9 @@ -(* Title: HoTT/HoTT_Base.thy - Author: Joshua Chen +(* +Title: HoTT_Base.thy +Author: Joshua Chen +Date: 2018 -Basic setup of a homotopy type theory object logic with a Russell-style cumulative universe hierarchy. +Basic setup of a homotopy type theory object logic with a cumulative Russell-style universe hierarchy. *) theory HoTT_Base @@ -49,8 +51,8 @@ Using method @{method rule} with @{thm U_cumulative} is unsafe, if applied blind One should instead use @{method elim}, or instantiate @{thm U_cumulative} suitably. \<close> -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> +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> @@ -59,22 +61,23 @@ abbreviation (input) constrained :: "[t \<Rightarrow> t, t, t] \<Rightarrow> pro where "f: A \<longrightarrow> B \<equiv> (\<And>x. x : A \<Longrightarrow> f x: B)" 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. +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 tf = "t \<Rightarrow> t" \<comment> \<open>Type of type families.\<close> +type_synonym tf = "t \<Rightarrow> t" \<comment> \<open>Type of type families\<close> section \<open>Named theorems\<close> +named_theorems comp + 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. +@{attribute comp} declares computation rules. +These are used by the \<open>compute\<close> method, and may also be passed to invocations of the method \<open>subst\<close> to perform equational rewriting. \<close> -named_theorems wellform -named_theorems comp +(* Todo: Set up the simplifier! *) end diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index abb6dda..9849195 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -1,63 +1,51 @@ -(* Title: HoTT/HoTT_Methods.thy - Author: Josh Chen +(* +Title: HoTT_Methods.thy +Author: Joshua Chen +Date: 2018 -Method setup for the HoTT library. Relies heavily on Eisbach. +Method setup for the HoTT logic. Relies heavily on Eisbach. *) theory HoTT_Methods - imports - "HOL-Eisbach.Eisbach" - "HOL-Eisbach.Eisbach_Tools" - HoTT_Base +imports + "HOL-Eisbach.Eisbach" + "HOL-Eisbach.Eisbach_Tools" + HoTT_Base + begin section \<open>Deriving typing judgments\<close> -method routine uses lems = (assumption | rule lems | standard)+ - -text " - @{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. -" - -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>. - \<open>wellform\<close> is like \<open>wellformed'\<close> but takes multiple judgments. - - The named theorem \<open>wellform\<close> is declared in HoTT_Base.thy. -" +method routine uses add = (assumption | rule add | rule)+ -method wellformed' uses jdmt declares wellform = - match wellform in rl: "PROP ?P" \<Rightarrow> \<open>( - catch \<open>rule rl[OF jdmt]\<close> \<open>fail\<close> | - catch \<open>wellformed' jdmt: rl[OF jdmt]\<close> \<open>fail\<close> - )\<close> - -method wellformed uses lems = - match lems in lem: "?X : ?Y" \<Rightarrow> \<open>wellformed' jdmt: lem\<close> +text \<open> +The method @{method routine} proves type judgments @{prop "a : A"} using the rules declared @{attribute intro} in the respective theory files, as well as additional provided lemmas passed using the modifier \<open>add\<close>. +\<close> section \<open>Substitution and simplification\<close> -text "Import the \<open>subst\<close> method, used for substituting definitional equalities." - ML_file "~~/src/Tools/misc_legacy.ML" ML_file "~~/src/Tools/IsaPlanner/isand.ML" ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML" ML_file "~~/src/Tools/IsaPlanner/zipper.ML" ML_file "~~/src/Tools/eqsubst.ML" -text "Perform basic single-step computations:" +\<comment> \<open>Import the @{method subst} method, used for substituting definitional equalities.\<close> -method compute uses lems = (subst lems comp | rule lems comp) +method compute declares comp = (subst comp) +text \<open> +Method @{method compute} performs single-step simplifications, using any rules declared @{attribute comp} in the context. +Premises of the rule(s) applied are added as new subgoals. +\<close> section \<open>Derivation search\<close> -text " Combine \<open>routine\<close>, \<open>wellformed\<close>, and \<open>compute\<close> to search for derivations of judgments." +text \<open>Combine @{method routine} and @{method compute} to search for derivations of judgments.\<close> -method derive uses lems = (routine lems: lems | compute lems: lems | wellformed lems: lems)+ +method derive uses lems = (routine add: lems | compute comp: lems)+ section \<open>Induction\<close> @@ -1,54 +1,48 @@ -(* Title: HoTT/Nat.thy - Author: Josh Chen +(* +Title: Nat.thy +Author: Joshua Chen +Date: 2018 Natural numbers *) theory Nat - imports HoTT_Base -begin +imports HoTT_Base +begin -section \<open>Constants and type rules\<close> axiomatization - Nat :: t ("\<nat>") and - zero :: t ("0") and - succ :: "t \<Rightarrow> t" and + 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 - Nat_intro_0: "0: \<nat>" -and - Nat_intro_succ: "n: \<nat> \<Longrightarrow> succ n: \<nat>" -and + Nat_form: "\<nat>: U O" and + + Nat_intro_0: "0: \<nat>" and + + Nat_intro_succ: "n: \<nat> \<Longrightarrow> succ n: \<nat>" and + Nat_elim: "\<lbrakk> - C: \<nat> \<longrightarrow> U i; - \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n); a: C 0; - n: \<nat> - \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a n: C n" -and + n: \<nat>; + C: \<nat> \<longrightarrow> U i; + \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>n c. f n c) a n: C n" and + Nat_comp_0: "\<lbrakk> + a: C 0; C: \<nat> \<longrightarrow> U i; - \<And>n c. \<lbrakk>n: \<nat>; c: C(n)\<rbrakk> \<Longrightarrow> f n c: C (succ n); - a: C 0 - \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a 0 \<equiv> a" -and + \<And>n c. \<lbrakk>n: \<nat>; c: C(n)\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>n c. f n c) a 0 \<equiv> a" and + Nat_comp_succ: "\<lbrakk> - C: \<nat> \<longrightarrow> U i; - \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n); a: C 0; - n: \<nat> - \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a (succ n) \<equiv> f n (ind\<^sub>\<nat> f a n)" - - -text "Rule attribute declarations:" + n: \<nat>; + C: \<nat> \<longrightarrow> U i; + \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>n c. f n c) a (succ n) \<equiv> f n (ind\<^sub>\<nat> f a n)" -lemmas Nat_intro = Nat_intro_0 Nat_intro_succ -lemmas Nat_comp [comp] = Nat_comp_0 Nat_comp_succ -lemmas Nat_routine [intro] = Nat_form Nat_intro Nat_elim +lemmas Nat_routine [intro] = Nat_form Nat_intro_0 Nat_intro_succ Nat_elim +lemmas Nat_comps [comp] = Nat_comp_0 Nat_comp_succ end @@ -1,62 +1,46 @@ -(* Title: HoTT/Proj.thy - Author: Josh Chen +(* +Title: Proj.thy +Author: Joshua Chen +Date: 2018 Projection functions \<open>fst\<close> and \<open>snd\<close> for the dependent sum type. *) theory Proj - imports - HoTT_Methods - Prod - Sum -begin +imports + HoTT_Methods + Prod + Sum +begin -definition fst :: "Term \<Rightarrow> Term" where "fst p \<equiv> ind\<^sub>\<Sum> (\<lambda>x y. x) p" -definition snd :: "Term \<Rightarrow> Term" where "snd p \<equiv> ind\<^sub>\<Sum> (\<lambda>x y. y) p" -text "Typing judgments and computation rules for the dependent and non-dependent projection functions." +definition fst :: "t \<Rightarrow> t" where "fst p \<equiv> ind\<^sub>\<Sum> (\<lambda>x y. x) p" +definition snd :: "t \<Rightarrow> t" where "snd p \<equiv> ind\<^sub>\<Sum> (\<lambda>x y. y) p" lemma fst_type: - assumes "\<Sum>x:A. B x: U i" and "p: \<Sum>x:A. B x" shows "fst p: A" + assumes "A: U i" and "B: A \<longrightarrow> U i" and "p: \<Sum>x:A. B x" shows "fst p: A" unfolding fst_def by (derive lems: assms) lemma fst_comp: assumes "A: U i" and "B: A \<longrightarrow> U i" and "a: A" and "b: B a" shows "fst <a,b> \<equiv> a" -unfolding fst_def -proof compute - show "a: A" and "b: B a" by fact+ -qed (routine lems: assms)+ +unfolding fst_def by compute (derive lems: assms) lemma snd_type: - assumes "\<Sum>x:A. B x: U i" and "p: \<Sum>x:A. B x" shows "snd p: B (fst p)" -unfolding snd_def -proof + assumes "A: U i" and "B: A \<longrightarrow> U i" and "p: \<Sum>x:A. B x" shows "snd p: B (fst p)" +unfolding snd_def proof show "\<And>p. p: \<Sum>x:A. B x \<Longrightarrow> B (fst p): U i" by (derive lems: assms fst_type) - fix x y - assume asm: "x: A" "y: B x" - show "y: B (fst <x,y>)" - proof (subst fst_comp) - show "A: U i" by (wellformed lems: assms(1)) - show "\<And>x. x: A \<Longrightarrow> B x: U i" by (wellformed lems: assms(1)) - qed fact+ + fix x y assume asm: "x: A" "y: B x" + show "y: B (fst <x,y>)" by (derive lems: asm assms fst_comp) qed fact lemma snd_comp: assumes "A: U i" and "B: A \<longrightarrow> U i" and "a: A" and "b: B a" shows "snd <a,b> \<equiv> b" -unfolding snd_def -proof compute - show "\<And>x y. y: B x \<Longrightarrow> y: B x" . - show "a: A" by fact - show "b: B a" by fact -qed (routine lems: assms) - - -text "Rule attribute declarations:" +unfolding snd_def by (derive lems: assms) -lemmas Proj_type [intro] = fst_type snd_type -lemmas Proj_comp [comp] = fst_comp snd_comp +lemmas Proj_types [intro] = fst_type snd_type +lemmas Proj_comps [comp] = fst_comp snd_comp end @@ -1,69 +1,58 @@ -(* Title: HoTT/Sum.thy - Author: Josh Chen +(* +Title: Sum.thy +Author: Joshua Chen +Date: 2018 Dependent sum type *) theory Sum - imports HoTT_Base -begin +imports HoTT_Base +begin -section \<open>Constants and syntax\<close> axiomatization - Sum :: "[t, Typefam] \<Rightarrow> t" and - pair :: "[t, t] \<Rightarrow> t" ("(1<_,/ _>)") and + Sum :: "[t, tf] \<Rightarrow> t" and + pair :: "[t, t] \<Rightarrow> t" ("(1<_,/ _>)") and indSum :: "[[t, t] \<Rightarrow> t, t] \<Rightarrow> t" ("(1ind\<^sub>\<Sum>)") syntax - "_SUM" :: "[idt, t, t] \<Rightarrow> t" ("(3\<Sum>_:_./ _)" 20) - "_SUM_ASCII" :: "[idt, t, t] \<Rightarrow> t" ("(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)" "SUM x:A. B" \<rightharpoonup> "CONST Sum A (\<lambda>x. B)" -text "Nondependent pair." - abbreviation Pair :: "[t, t] \<Rightarrow> t" (infixr "\<times>" 50) where "A \<times> B \<equiv> \<Sum>_:A. B" +axiomatization where +\<comment> \<open>Type rules\<close> -section \<open>Type rules\<close> + Sum_form: "\<lbrakk>A: U i; B: A \<longrightarrow> U i\<rbrakk> \<Longrightarrow> \<Sum>x:A. B x: U i" and + + Sum_intro: "\<lbrakk>B: A \<longrightarrow> U i; a: A; b: B a\<rbrakk> \<Longrightarrow> <a,b>: \<Sum>x:A. B x" and -axiomatization where - Sum_form: "\<lbrakk>A: U i; B: A \<longrightarrow> U i\<rbrakk> \<Longrightarrow> \<Sum>x:A. B x: U i" -and - Sum_intro: "\<lbrakk>B: A \<longrightarrow> U i; a: A; b: B a\<rbrakk> \<Longrightarrow> <a,b>: \<Sum>x:A. B x" -and Sum_elim: "\<lbrakk> p: \<Sum>x:A. B x; - \<And>x y. \<lbrakk>x: A; y: B x\<rbrakk> \<Longrightarrow> f x y: C <x,y>; - C: \<Sum>x:A. B x \<longrightarrow> U i - \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum> f p: C p" (* What does writing \<lambda>x y. f(x, y) change? *) -and + C: \<Sum>x:A. B x \<longrightarrow> U i; + \<And>x y. \<lbrakk>x: A; y: B x\<rbrakk> \<Longrightarrow> f x y: C <x,y> \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum> (\<lambda>x y. f x y) p: C p" and + Sum_comp: "\<lbrakk> a: A; b: B a; - \<And>x y. \<lbrakk>x: A; y: B(x)\<rbrakk> \<Longrightarrow> f x y: C <x,y>; B: A \<longrightarrow> U i; - C: \<Sum>x:A. B x \<longrightarrow> U i - \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum> f <a,b> \<equiv> f a b" - -text "Admissible inference rules for sum formation:" - -axiomatization where - Sum_wellform1: "(\<Sum>x:A. B x: U i) \<Longrightarrow> A: U i" -and - Sum_wellform2: "(\<Sum>x:A. B x: U i) \<Longrightarrow> B: A \<longrightarrow> U i" + C: \<Sum>x:A. B x \<longrightarrow> U i; + \<And>x y. \<lbrakk>x: A; y: B(x)\<rbrakk> \<Longrightarrow> f x y: C <x,y> \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum> (\<lambda>x y. f x y) <a,b> \<equiv> f a b" and +\<comment> \<open>Congruence rules\<close> -text "Rule attribute declarations:" + Sum_form_eq: "\<lbrakk>A: U i; B: A \<longrightarrow> U i; C: A \<longrightarrow> U i; \<And>x. x: A \<Longrightarrow> B x \<equiv> C x\<rbrakk> \<Longrightarrow> \<Sum>x:A. B x \<equiv> \<Sum>x:A. C x" -lemmas Sum_comp [comp] -lemmas Sum_wellform [wellform] = Sum_wellform1 Sum_wellform2 lemmas Sum_routine [intro] = Sum_form Sum_intro Sum_elim +lemmas Sum_comp [comp] end @@ -1,33 +1,31 @@ -(* Title: HoTT/Unit.thy - Author: Josh Chen +(* +Title: Unit.thy +Author: Joshua Chen +Date: 2018 Unit type *) theory Unit - imports HoTT_Base -begin +imports HoTT_Base +begin -section \<open>Constants and type rules\<close> axiomatization - Unit :: Term ("\<one>") and - pt :: Term ("\<star>") and - indUnit :: "[Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>\<one>)") + Unit :: t ("\<one>") and + pt :: t ("\<star>") and + indUnit :: "[t, t] \<Rightarrow> t" ("(1ind\<^sub>\<one>)") where - Unit_form: "\<one>: U O" -and - Unit_intro: "\<star>: \<one>" -and - Unit_elim: "\<lbrakk>C: \<one> \<longrightarrow> U i; c: C \<star>; a: \<one>\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c a: C a" -and - Unit_comp: "\<lbrakk>C: \<one> \<longrightarrow> U i; c: C \<star>\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c \<star> \<equiv> c" + Unit_form: "\<one>: U O" and + Unit_intro: "\<star>: \<one>" and -text "Rule attribute declarations:" + Unit_elim: "\<lbrakk>a: \<one>; c: C \<star>; C: \<one> \<longrightarrow> U i\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c a: C a" and + + Unit_comp: "\<lbrakk>c: C \<star>; C: \<one> \<longrightarrow> U i\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c \<star> \<equiv> c" -lemmas Unit_comp [comp] lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_elim +lemmas Unit_comp [comp] end |