aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2019-02-22 23:45:50 +0100
committerJosh Chen2019-02-22 23:45:50 +0100
commit57d183c7955fb54b3eb6dd431f5aec338131266b (patch)
treeae6bfabbd8fcd63ee7d5140ca842599efbd58c16
parent0036345412d5c145b63693ed672b175018fa3791 (diff)
Cleanups and reorganization
-rw-r--r--Coprod.thy50
-rw-r--r--Empty.thy27
-rw-r--r--Eq.thy27
-rw-r--r--Equal.thy219
-rw-r--r--HoTT.thy28
-rw-r--r--HoTT_Methods.thy5
-rw-r--r--More_Types.thy83
-rw-r--r--Nat.thy45
-rw-r--r--Prod.thy34
-rw-r--r--Unit.thy32
10 files changed, 153 insertions, 397 deletions
diff --git a/Coprod.thy b/Coprod.thy
deleted file mode 100644
index b0a1ad2..0000000
--- a/Coprod.thy
+++ /dev/null
@@ -1,50 +0,0 @@
-(*
-Title: Coprod.thy
-Author: Joshua Chen
-Date: 2018
-
-Coproduct type
-*)
-
-theory Coprod
-imports HoTT_Base
-
-begin
-
-
-axiomatization
- 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_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) \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d 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) \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d (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) \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d (inr b) \<equiv> d b"
-
-lemmas Coprod_form [form]
-lemmas Coprod_routine [intro] = Coprod_form Coprod_intro_inl Coprod_intro_inr Coprod_elim
-lemmas Coprod_comp [comp] = Coprod_comp_inl Coprod_comp_inr
-
-
-end
diff --git a/Empty.thy b/Empty.thy
deleted file mode 100644
index ee11045..0000000
--- a/Empty.thy
+++ /dev/null
@@ -1,27 +0,0 @@
-(*
-Title: Empty.thy
-Author: Joshua Chen
-Date: 2018
-
-Empty type
-*)
-
-theory Empty
-imports HoTT_Base
-
-begin
-
-
-axiomatization
- Empty :: t ("\<zero>") and
- indEmpty :: "t \<Rightarrow> t" ("(1ind\<^sub>\<zero>)")
-where
- Empty_form: "\<zero>: U O" and
-
- Empty_elim: "\<lbrakk>a: \<zero>; C: \<zero> \<longrightarrow> U i\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero> a: C a"
-
-lemmas Empty_form [form]
-lemmas Empty_routine [intro] = Empty_form Empty_elim
-
-
-end
diff --git a/Eq.thy b/Eq.thy
index e93dd8a..7783682 100644
--- a/Eq.thy
+++ b/Eq.thy
@@ -54,6 +54,9 @@ method path_ind for a b p :: t =
method path_ind' for C :: "[t, t, t] \<Rightarrow> t" =
(rule Eq_elim[where ?C=C]; (assumption | fact)?)
+syntax "_induct_over" :: "[idt, idt, idt, t] \<Rightarrow> [t, t, t] \<Rightarrow> t" ("(2{_, _, _}/ _)" 0)
+translations "{x, y, p} C" \<rightleftharpoons> "\<lambda>x y p. C"
+
section \<open>Properties of equality\<close>
@@ -180,8 +183,12 @@ qed (routine add: assms)
text \<open>
We use the proof of associativity of path composition to demonstrate the process of deriving proof terms.
-The proof involves a triply-nested path induction, which is cumbersome to write in a structured style, especially if one does not know the form of the proof term in the first place.
+The proof involves a triply-nested path induction, which is cumbersome to write in a structured style, especially if one does not know the correct form of the proof term in the first place.
However, using proof scripts the derivation becomes quite easy; we simply give the correct form of the statements to induct over, and prove the simple subgoals returned by the prover.
+
+The proof is sensitive to the order of the quantifiers in the product.
+In particular, changing the order causes unification to fail in the path inductions.
+It seems to be good practice to order the variables in the order over which we will path-induct.
\<close>
declare[[pretty_pathcomp=false]]
@@ -193,22 +200,22 @@ schematic_goal pathcomp_assoc:
pathcomp A x y w p (pathcomp A y z w q r) =[x =[A] w]
pathcomp A x z w (pathcomp A x y z p q) r"
apply (quantify 3)
- apply (path_ind'
- "\<lambda>x y p. \<Prod>(z: A). \<Prod>(q: y =[A] z). \<Prod>(w: A). \<Prod>(r: z =[A] w).
+ apply (path_ind' "{x, y, p}
+ \<Prod>(z: A). \<Prod>(q: y =[A] z). \<Prod>(w: A). \<Prod>(r: z =[A] w).
Eq.pathcomp A x y w p (Eq.pathcomp A y z w q r) =[x =[A] w]
Eq.pathcomp A x z w (Eq.pathcomp A x y z p q) r")
apply (quantify 2)
- apply (path_ind'
- "\<lambda>xa z q. \<Prod>(w: A). \<Prod>(r: z =[A] w).
+ apply (path_ind' "{xa, z, q}
+ \<Prod>(w: A). \<Prod>(r: z =[A] w).
Eq.pathcomp A xa xa w (refl xa) (Eq.pathcomp A xa z w q r) =[xa =[A] w]
Eq.pathcomp A xa z w (Eq.pathcomp A xa xa z (refl xa) q) r")
apply (quantify 2)
- apply (path_ind'
- "\<lambda>xb w r. Eq.pathcomp A xb xb w (refl xb) (Eq.pathcomp A xb xb w (refl xb) r) =[xb =[A] w]
+ apply (path_ind' "{xb, w, r}
+ Eq.pathcomp A xb xb w (refl xb) (Eq.pathcomp A xb xb w (refl xb) r) =[xb =[A] w]
Eq.pathcomp A xb xb w (Eq.pathcomp A xb xb xb (refl xb) (refl xb)) r")
-
- text \<open>\<close>
-
+
+ text \<open>And now the rest is routine.\<close>
+
apply (derive; (rule assms|assumption)?)
apply (compute, rule assms, assumption)+
apply (elim Eq_intro, rule Eq_intro, assumption)
diff --git a/Equal.thy b/Equal.thy
deleted file mode 100644
index 17c1c99..0000000
--- a/Equal.thy
+++ /dev/null
@@ -1,219 +0,0 @@
-(********
-Isabelle/HoTT: Equality
-Feb 2019
-
-********)
-
-theory Equal
-imports Prod HoTT_Methods
-
-begin
-
-
-section \<open>Type definitions\<close>
-
-axiomatization
- Eq :: "[t, t, t] \<Rightarrow> t" and
- refl :: "t \<Rightarrow> t" and
- indEq :: "[[t, t, t] \<Rightarrow> t, t \<Rightarrow> t, t, t, t] \<Rightarrow> t"
-
-syntax
- "_Eq" :: "[t, t, t] \<Rightarrow> t" ("(3_ =[_]/ _)" [101, 0, 101] 100)
-translations
- "a =[A] b" \<rightleftharpoons> "(CONST Eq) A a b"
-
-axiomatization where
- Eq_form: "\<lbrakk>A: U i; a: A; b: A\<rbrakk> \<Longrightarrow> a =[A] b: U i" and
-
- Eq_intro: "a: A \<Longrightarrow> (refl a): a =[A] a" and
-
- Eq_elim: "\<lbrakk>
- p: x =[A] y;
- a: A;
- b: A;
- \<And>x. x: A \<Longrightarrow> f x: C x x (refl x);
- \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =[A] y \<leadsto> U i \<rbrakk> \<Longrightarrow> indEq C f a b p : C a b p" and
-
- Eq_comp: "\<lbrakk>
- a: A;
- \<And>x. x: A \<Longrightarrow> f x: C x x (refl x);
- \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =[A] y \<leadsto> U i \<rbrakk> \<Longrightarrow> indEq C f a a (refl a) \<equiv> f a"
-
-lemmas Eq_form [form]
-lemmas Eq_routine [intro] = Eq_form Eq_intro Eq_elim
-lemmas Eq_comp [comp]
-
-
-section \<open>Path induction\<close>
-
-text \<open>We set up rudimentary automation of path induction:\<close>
-
-method path_ind for a b p :: t =
- (rule Eq_elim[where ?a=a and ?b=b and ?p=p]; (fact | assumption)?)
-
-
-section \<open>Properties of equality\<close>
-
-subsection \<open>Symmetry (path inverse)\<close>
-
-definition inv :: "[t, t, t, t] \<Rightarrow> t"
-where "inv A x y p \<equiv> indEq (\<lambda>x y. ^(y =[A] x)) (\<lambda>x. refl x) x y p"
-
-syntax "_inv" :: "t \<Rightarrow> t" ("~_" [1000])
-
-text \<open>Pretty-printing switch for path inverse:\<close>
-
-ML \<open>val pretty_inv = Attrib.setup_config_bool @{binding "pretty_inv"} (K true)\<close>
-
-print_translation \<open>
-let fun inv_tr' ctxt [A, x, y, p] =
- if Config.get ctxt pretty_inv
- then Syntax.const @{syntax_const "_inv"} $ p
- else @{const inv} $ A $ x $ y $ p
-in
- [(@{const_syntax inv}, inv_tr')]
-end
-\<close>
-
-lemma inv_type: "\<lbrakk>A: U i; x: A; y: A; p: x =[A] y\<rbrakk> \<Longrightarrow> inv A x y p: y =[A] x"
-unfolding inv_def by derive
-
-lemma inv_comp: "\<lbrakk>A: U i; a: A\<rbrakk> \<Longrightarrow> inv A a a (refl a) \<equiv> refl a"
-unfolding inv_def by derive
-
-declare
- inv_type [intro]
- inv_comp [comp]
-
-subsection \<open>Transitivity (path composition)\<close>
-
-schematic_goal transitivity:
- assumes "A: U i" "x: A" "y: A" "p: x =[A] y"
- shows "?p: \<Prod>z: A. y =[A]z \<rightarrow> x =[A] z"
-proof (path_ind x y p, quantify_all)
- fix x z show "\<And>p. p: x =[A] z \<Longrightarrow> p: x =[A] z" .
-qed (routine add: assms)
-
-definition pathcomp :: "[t, t, t, t, t, t] \<Rightarrow> t"
-where
- "pathcomp A x y z p q \<equiv>
- (indEq (\<lambda>x y _. \<Prod>z: A. y =[A] z \<rightarrow> x =[A] z) (\<lambda>x. \<lambda>y: A. id (x =[A] y)) x y p)`z`q"
-
-syntax "_pathcomp" :: "[t, t] \<Rightarrow> t" (infixl "*" 110)
-
-text \<open>Pretty-printing switch for path composition:\<close>
-
-ML \<open>val pretty_pathcomp = Attrib.setup_config_bool @{binding "pretty_pathcomp"} (K true)\<close>
-
-print_translation \<open>
-let fun pathcomp_tr' ctxt [A, x, y, z, p, q] =
- if Config.get ctxt pretty_pathcomp
- then Syntax.const @{syntax_const "_pathcomp"} $ p $ q
- else @{const pathcomp} $ A $ x $ y $ z $ p $ q
-in
- [(@{const_syntax pathcomp}, pathcomp_tr')]
-end
-\<close>
-
-lemma pathcomp_type:
- assumes "A: U i" "x: A" "y: A" "z: A" "p: x =[A] y" "q: y =[A] z"
- shows "pathcomp A x y z p q: x =[A] z"
-unfolding pathcomp_def by (routine add: transitivity assms)
-
-lemma pathcomp_cmp:
- assumes "A: U i" and "a: A"
- shows "pathcomp A a a a (refl a) (refl a) \<equiv> refl a"
-unfolding pathcomp_def by (derive lems: assms)
-
-lemmas pathcomp_type [intro]
-lemmas pathcomp_comp [comp] = pathcomp_cmp
-
-
-section \<open>Higher groupoid structure of types\<close>
-
-schematic_goal pathcomp_idr:
- assumes "A: U i" "x: A" "y: A" "p: x =[A] y"
- shows "?a: pathcomp A x y y p (refl y) =[x =[A] y] p"
-proof (path_ind x y p)
- show "\<And>x. x: A \<Longrightarrow> refl(refl x): pathcomp A x x x (refl x) (refl x) =[x =[A] x] (refl x)"
- by (derive lems: assms)
-qed (routine add: assms)
-
-schematic_goal pathcomp_idl:
- assumes "A: U i" "x: A" "y: A" "p: x =[A] y"
- shows "?a: pathcomp A x x y (refl x) p =[x =[A] y] p"
-proof (path_ind x y p)
- show "\<And>x. x: A \<Longrightarrow> refl(refl x): pathcomp A x x x (refl x) (refl x) =[x =[A] x] (refl x)"
- by (derive lems: assms)
-qed (routine add: assms)
-
-schematic_goal pathcomp_invr:
- assumes "A: U i" "x: A" "y: A" "p: x =[A] y"
- shows "?a: pathcomp A x y x p (inv A x y p) =[x =[A] x] (refl x)"
-proof (path_ind x y p)
- show
- "\<And>x. x: A \<Longrightarrow> refl(refl x):
- pathcomp A x x x (refl x) (inv A x x (refl x)) =[x =[A] x] (refl x)"
- by (derive lems: assms)
-qed (routine add: assms)
-
-schematic_goal pathcomp_invl:
- assumes "A: U i" "x: A" "y: A" "p: x =[A] y"
- shows "?a: pathcomp A y x y (inv A x y p) p =[y =[A] y] refl(y)"
-proof (path_ind x y p)
- show
- "\<And>x. x: A \<Longrightarrow> refl(refl x):
- pathcomp A x x x (inv A x x (refl x)) (refl x) =[x =[A] x] (refl x)"
- by (derive lems: assms)
-qed (routine add: assms)
-
-schematic_goal inv_involutive:
- assumes "A: U i" "x: A" "y: A" "p: x =[A] y"
- shows "?a: inv A y x (inv A x y p) =[x =[A] y] p"
-proof (path_ind x y p)
- show "\<And>x. x: A \<Longrightarrow> refl(refl x): inv A x x (inv A x x (refl x)) =[x =[A] x] (refl x)"
- by (derive lems: assms)
-qed (routine add: assms)
-
-declare[[pretty_pathcomp=false]]
-
-schematic_goal pathcomp_assoc:
- assumes "A: U i" "x: A" "y: A" "z: A" "w: A" "p: x =[A] y"
- shows
- "?a: \<Prod>q: y =[A] z. \<Prod>r: z =[A] w.
- pathcomp A x y w p (pathcomp A y z w q r) =[x =[A] w]
- pathcomp A x z w (pathcomp A x y z p q) r"
-proof (path_ind x y p)
- oops
- schematic_goal l:
- assumes "A: U i" "x: A" "z: A" "w: A" "q: x =[A] z"
- shows
- "?a: \<Prod>r: z =[A] w. pathcomp A x x w (refl x) (pathcomp A y z w q r) =[x =[A] w]
- pathcomp A x z w (pathcomp A x x z (refl x) q) r"
- proof (path_ind x z q)
- oops
- schematic_goal l':
- assumes "A: U i" "x: A" "w: A" "r: x =[A] w"
- shows
- "?a: pathcomp A x x w (refl x) (pathcomp A x x w (refl x) r) =[x =[A] w]
- pathcomp A x x w (pathcomp A x x x (refl x) (refl x)) r"
- proof (path_ind x w r)
- show "\<And>x. x: A \<Longrightarrow> refl(refl x):
- pathcomp A x x x (refl x) (pathcomp A x x x (refl x) (refl x)) =[x =[A] x]
- pathcomp A x x x (pathcomp A x x x (refl x) (refl x)) (refl x)"
- by (derive lems: assms)
- qed (routine add: assms)
-
-(* Possible todo:
- implement a custom version of schematic_goal/theorem that exports the derived proof term.
-*)
-
-definition l'_prftm :: "[t, t, t, t] \<Rightarrow> t"
-where "l'_prftm A x w r\<equiv>
- indEq
- (\<lambda>a b c. pathcomp A a a b (refl a) (pathcomp A a a b (refl a) c) =[a =[A] b]
- pathcomp A a a b (pathcomp A a a a (refl a) (refl a)) c)
- (\<lambda>x. refl (refl x)) x w r"
-
-
-end
diff --git a/HoTT.thy b/HoTT.thy
index 6c6ad21..e5db673 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -1,44 +1,40 @@
-(*
-Title: HoTT.thy
-Author: Joshua Chen
-Date: 2018
+(********
+Isabelle/HoTT
+Feb 2019
-Homotopy type theory
-*)
+An experimental implementation of homotopy type theory.
+
+********)
theory HoTT
imports
+
(* Basic theories *)
HoTT_Base
HoTT_Methods
(* Types *)
-Coprod
-Empty
-Equal
+Eq
Nat
Prod
Sum
-Unit
+More_Types
(* Derived definitions and properties *)
-Equality
Projections
Univalence
begin
-
text \<open>Rule bundles:\<close>
lemmas intros =
- Nat_intro_0 Nat_intro_succ Prod_intro Sum_intro Equal_intro Coprod_intro_inl Coprod_intro_inr Unit_intro
+ Nat_intro_0 Nat_intro_succ Prod_intro Sum_intro Eq_intro Cprd_intro_inl Cprd_intro_inr Unit_intro
lemmas elims =
- Nat_elim Prod_elim Sum_elim Equal_elim Coprod_elim Unit_elim Empty_elim
+ Nat_elim Prod_elim Sum_elim Eq_elim Cprd_elim Unit_elim Null_elim
lemmas routines =
- Nat_routine Prod_routine Sum_routine Equal_routine Coprod_routine Unit_routine Empty_routine
-
+ Nat_routine Prod_routine Sum_routine Eq_routine Cprd_routine Unit_routine Null_routine
end
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index 099a73e..c9744e9 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -51,7 +51,7 @@ method cumulativity declares form = (
section \<open>Deriving typing judgments\<close>
-method routine uses add = (rule add | assumption | rule)+
+method routine uses add = (assumption | rule add | rule)+
text \<open>
The method @{method routine} proves typing judgments @{prop "a: A"} using the rules declared @{attribute intro} in the respective theory files, as well as any additional lemmas provided with the modifier @{theory_text add}.
@@ -65,7 +65,8 @@ The method @{theory_text derive} combines @{method routine} and @{method compute
It also handles universes using @{method hierarchy} and @{method cumulativity}.
\<close>
-method derive uses lems = (routine add: lems | compute comp: lems | cumulativity form: lems | hierarchy)+
+method derive uses lems =
+ (routine add: lems | compute comp: lems | cumulativity form: lems | hierarchy)+
section \<open>Additional method combinators\<close>
diff --git a/More_Types.thy b/More_Types.thy
new file mode 100644
index 0000000..9125aca
--- /dev/null
+++ b/More_Types.thy
@@ -0,0 +1,83 @@
+(********
+Isabelle/HoTT: Coproduct, unit, and empty types
+Feb 2019
+
+********)
+
+theory More_Types
+imports HoTT_Base
+
+begin
+
+
+section \<open>Coproduct type\<close>
+
+axiomatization
+ Cprd :: "[t, t] \<Rightarrow> t" (infixr "+" 50) and
+ inl :: "[t, t, t] \<Rightarrow> t" and
+ inr :: "[t, t, t] \<Rightarrow> t" and
+ indCprd :: "[t \<Rightarrow> t, t \<Rightarrow> t, t \<Rightarrow> t, t] \<Rightarrow> t"
+where
+ Cprd_form: "\<lbrakk>A: U i; B: U i\<rbrakk> \<Longrightarrow> A + B: U i" and
+
+ Cprd_intro_inl: "\<lbrakk>a: A; B: U i\<rbrakk> \<Longrightarrow> inl A B a: A + B" and
+
+ Cprd_intro_inr: "\<lbrakk>b: B; A: U i\<rbrakk> \<Longrightarrow> inr A B b: A + B" and
+
+ Cprd_elim: "\<lbrakk>
+ u: A + B;
+ C: A + B \<leadsto> U i;
+ \<And>x. x: A \<Longrightarrow> c x: C (inl A B x);
+ \<And>y. y: B \<Longrightarrow> d y: C (inr A B y) \<rbrakk> \<Longrightarrow> indCprd C c d u: C u" and
+
+ Cprd_cmp_inl: "\<lbrakk>
+ a: A;
+ C: A + B \<leadsto> U i;
+ \<And>x. x: A \<Longrightarrow> c x: C (inl A B x);
+ \<And>y. y: B \<Longrightarrow> d y: C (inr A B y) \<rbrakk> \<Longrightarrow> indCprd C c d (inl A B a) \<equiv> c a" and
+
+ Cprd_cmp_inr: "\<lbrakk>
+ b: B;
+ C: A + B \<leadsto> U i;
+ \<And>x. x: A \<Longrightarrow> c x: C (inl A B x);
+ \<And>y. y: B \<Longrightarrow> d y: C (inr A B y) \<rbrakk> \<Longrightarrow> indCprd C c d (inr A B b) \<equiv> d b"
+
+lemmas Cprd_form [form]
+lemmas Cprd_routine [intro] = Cprd_form Cprd_intro_inl Cprd_intro_inr Cprd_elim
+lemmas Cprd_comp [comp] = Cprd_cmp_inl Cprd_cmp_inr
+
+
+section \<open>Unit type\<close>
+
+axiomatization
+ Unit :: t and
+ pt :: t and
+ indUnit :: "[t \<Rightarrow> t, t, t] \<Rightarrow> t"
+where
+ Unit_form: "Unit: U O" and
+
+ Unit_intro: "pt: Unit" and
+
+ Unit_elim: "\<lbrakk>x: Unit; c: C pt; C: Unit \<leadsto> U i\<rbrakk> \<Longrightarrow> indUnit C c x: C x" and
+
+ Unit_cmp: "\<lbrakk>c: C Unit; C: Unit \<leadsto> U i\<rbrakk> \<Longrightarrow> indUnit C c pt \<equiv> c"
+
+lemmas Unit_form [form]
+lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_elim
+lemmas Unit_cmp [comp]
+
+
+section \<open>Empty type\<close>
+
+axiomatization
+ Null :: t and
+ indNull :: "[t \<Rightarrow> t, t] \<Rightarrow> t"
+where
+ Null_form: "Null: U O" and
+
+ Null_elim: "\<lbrakk>z: Null; C: Null \<leadsto> U i\<rbrakk> \<Longrightarrow> indNull C z: C z"
+
+lemmas Null_form [form]
+lemmas Null_routine [intro] = Null_form Null_elim
+
+end
diff --git a/Nat.thy b/Nat.thy
index 657e790..61e03e8 100644
--- a/Nat.thy
+++ b/Nat.thy
@@ -1,49 +1,46 @@
-(*
-Title: Nat.thy
-Author: Joshua Chen
-Date: 2018
+(********
+Isabelle/HoTT: Natural numbers
+Feb 2019
-Natural numbers
-*)
+********)
theory Nat
imports HoTT_Base
begin
-
axiomatization
- Nat :: t ("\<nat>") and
+ Nat :: t and
zero :: t ("0") and
succ :: "t \<Rightarrow> t" and
- indNat :: "[[t, t] \<Rightarrow> t, t, t] \<Rightarrow> t" ("(1ind\<^sub>\<nat>)")
+ indNat :: "[t \<Rightarrow> t, [t, t] \<Rightarrow> t, t, t] \<Rightarrow> t"
where
- Nat_form: "\<nat>: U O" and
+ Nat_form: "Nat: U O" and
- Nat_intro_0: "0: \<nat>" and
+ Nat_intro_0: "0: Nat" and
- Nat_intro_succ: "n: \<nat> \<Longrightarrow> succ n: \<nat>" and
+ Nat_intro_succ: "n: Nat \<Longrightarrow> succ n: Nat" and
Nat_elim: "\<lbrakk>
a: C 0;
- 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> f a n: C n" and
+ n: Nat;
+ C: Nat \<leadsto> U i;
+ \<And>n c. \<lbrakk>n: Nat; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> indNat C f a n: C n" and
- Nat_comp_0: "\<lbrakk>
+ Nat_cmp_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) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a 0 \<equiv> a" and
+ C: Nat \<leadsto> U i;
+ \<And>n c. \<lbrakk>n: Nat; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> indNat C f a 0 \<equiv> a" and
- Nat_comp_succ: "\<lbrakk>
+ Nat_cmp_succ: "\<lbrakk>
a: C 0;
- 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> f a (succ n) \<equiv> f n (ind\<^sub>\<nat> f a n)"
+ n: Nat;
+ C: Nat \<leadsto> U i;
+ \<And>n c. \<lbrakk>n: Nat; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n)
+ \<rbrakk> \<Longrightarrow> indNat C f a (succ n) \<equiv> f n (indNat C f a n)"
lemmas Nat_form [form]
lemmas Nat_routine [intro] = Nat_form Nat_intro_0 Nat_intro_succ Nat_elim
-lemmas Nat_comps [comp] = Nat_comp_0 Nat_comp_succ
-
+lemmas Nat_comps [comp] = Nat_cmp_0 Nat_cmp_succ
end
diff --git a/Prod.thy b/Prod.thy
index ff62ee6..059932c 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -70,23 +70,6 @@ lemmas Prod_comp [comp] = Prod_cmp Prod_uniq
lemmas Prod_cong [cong] = Prod_form_eq Prod_intro_eq
-section \<open>Universal quantification\<close>
-
-text \<open>
-It will often be useful to convert a proof goal asserting the inhabitation of a dependent product to one that instead uses Pure universal quantification.
-
-Method @{theory_text quantify_all} converts the goal
-@{text "t: \<Prod>x1: A1. ... \<Prod>xn: An. B x1 ... xn"},
-where @{term B} is not a product, to
-@{text "\<And>x1 ... xn . \<lbrakk>x1: A1; ...; xn: An\<rbrakk> \<Longrightarrow> ?b x1 ... xn: B x1 ... xn"}.
-
-Method @{theory_text "quantify k"} does the same, but only for the first k unknowns.
-\<close>
-
-method quantify_all = (rule Prod_intro)+
-method_setup quantify = \<open>repeat (fn ctxt => Method.rule_tac ctxt [@{thm Prod_intro}] [] 1)\<close>
-
-
section \<open>Function composition\<close>
definition compose :: "[t, t, t] \<Rightarrow> t"
@@ -146,4 +129,21 @@ by (derive lems: assms cong)
abbreviation id :: "t \<Rightarrow> t" where "id A \<equiv> \<lambda>x: A. x"
+
+section \<open>Universal quantification\<close>
+
+text \<open>
+It will often be useful to convert a proof goal asserting the inhabitation of a dependent product to one that instead uses Pure universal quantification.
+
+Method @{theory_text quantify_all} converts the goal
+@{text "t: \<Prod>x1: A1. ... \<Prod>xn: An. B x1 ... xn"},
+where @{term B} is not a product, to
+@{text "\<And>x1 ... xn . \<lbrakk>x1: A1; ...; xn: An\<rbrakk> \<Longrightarrow> ?b x1 ... xn: B x1 ... xn"}.
+
+Method @{theory_text "quantify k"} does the same, but only for the first k unknowns.
+\<close>
+
+method quantify_all = (rule Prod_intro)+
+method_setup quantify = \<open>repeat (fn ctxt => Method.rule_tac ctxt [@{thm Prod_intro}] [] 1)\<close>
+
end
diff --git a/Unit.thy b/Unit.thy
deleted file mode 100644
index 7c221f0..0000000
--- a/Unit.thy
+++ /dev/null
@@ -1,32 +0,0 @@
-(*
-Title: Unit.thy
-Author: Joshua Chen
-Date: 2018
-
-Unit type
-*)
-
-theory Unit
-imports HoTT_Base
-
-begin
-
-
-axiomatization
- 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>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_form [form]
-lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_elim
-lemmas Unit_comp [comp]
-
-end