aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2018-09-17 13:13:55 +0200
committerJosh Chen2018-09-17 13:13:55 +0200
commit76ac8ed82317f3f62f26ecc88f412c61004bcffa (patch)
tree02f3f3f5f87027d38520e376c577e7e6621fa6cf
parentea0c0c5427888982adce10ab25cebe445997f08b (diff)
Reorganizing theories
Diffstat (limited to '')
-rw-r--r--Coprod.thy64
-rw-r--r--Empty.thy22
-rw-r--r--HoTT.thy2
-rw-r--r--HoTT_Base.thy25
-rw-r--r--HoTT_Methods.thy56
-rw-r--r--Nat.thy60
-rw-r--r--Proj.thy56
-rw-r--r--Sum.thy57
-rw-r--r--Unit.thy32
9 files changed, 155 insertions, 219 deletions
diff --git a/Coprod.thy b/Coprod.thy
index 97e0566..d97228e 100644
--- a/Coprod.thy
+++ b/Coprod.thy
@@ -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
diff --git a/Empty.thy b/Empty.thy
index 107f2d7..3060867 100644
--- a/Empty.thy
+++ b/Empty.thy
@@ -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
diff --git a/HoTT.thy b/HoTT.thy
index abb1085..3f2d475 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -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>
diff --git a/Nat.thy b/Nat.thy
index a82e7cb..46b1af5 100644
--- a/Nat.thy
+++ b/Nat.thy
@@ -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
diff --git a/Proj.thy b/Proj.thy
index 74c561c..f272224 100644
--- a/Proj.thy
+++ b/Proj.thy
@@ -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
diff --git a/Sum.thy b/Sum.thy
index 92375b9..422e01b 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -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
diff --git a/Unit.thy b/Unit.thy
index 6760f27..61c6439 100644
--- a/Unit.thy
+++ b/Unit.thy
@@ -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