aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Coprod.thy40
-rw-r--r--Equal.thy34
-rw-r--r--HoTT_Base.thy4
-rw-r--r--Nat.thy30
-rw-r--r--Prod.thy12
-rw-r--r--Sum.thy28
-rw-r--r--scratch.thy4
7 files changed, 74 insertions, 78 deletions
diff --git a/Coprod.thy b/Coprod.thy
index 75e621a..a301e7e 100644
--- a/Coprod.thy
+++ b/Coprod.thy
@@ -14,43 +14,43 @@ section \<open>Constants and type rules\<close>
axiomatization
Coprod :: "[Term, Term] \<Rightarrow> Term" (infixr "+" 50) and
- inl :: "Term \<Rightarrow> Term" ("(1inl'(_'))") and
- inr :: "Term \<Rightarrow> Term" ("(1inr'(_'))") and
- indCoprod :: "[Term, Term, Typefam, Term \<Rightarrow> Term, Term \<Rightarrow> Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>+[_,/ _])")
+ inl :: "Term \<Rightarrow> Term" and
+ inr :: "Term \<Rightarrow> Term" and
+ indCoprod :: "[Term \<Rightarrow> Term, Term \<Rightarrow> Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>+)")
where
- Coprod_form: "\<And>i A B. \<lbrakk>A : U(i); B : U(i)\<rbrakk> \<Longrightarrow> A + B : U(i)"
+ Coprod_form: "\<And>i A B. \<lbrakk>A : U(i); B : U(i)\<rbrakk> \<Longrightarrow> A + B: U(i)"
and
- Coprod_intro1: "\<And>A B a b. \<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> inl(a) : A + B"
+ Coprod_intro1: "\<And>A B a b. \<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> inl(a): A + B"
and
- Coprod_intro2: "\<And>A B a b. \<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> inr(b) : A + B"
+ Coprod_intro2: "\<And>A B a b. \<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> inr(b): A + B"
and
Coprod_elim: "\<And>i A B C c d e. \<lbrakk>
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);
- e : A + B
- \<rbrakk> \<Longrightarrow> ind\<^sub>+[A,B] C c d e : C e"
+ \<And>x. x: A \<Longrightarrow> c(x): C(inl(x));
+ \<And>y. y: B \<Longrightarrow> d(y): C(inr(y));
+ e: A + B
+ \<rbrakk> \<Longrightarrow> ind\<^sub>+(c)(d)(e) : C(e)"
and
Coprod_comp1: "\<And>i A B C c d a. \<lbrakk>
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>+[A,B] C c d inl(a) \<equiv> c a"
+ \<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
Coprod_comp2: "\<And>i A B C c d b. \<lbrakk>
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>+[A,B] C c d inr(b) \<equiv> d b"
+ \<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_form_cond1: "\<And>i A B. A + B : U(i) \<Longrightarrow> A : U(i)"
+ Coprod_form_cond1: "\<And>i A B. A + B: U(i) \<Longrightarrow> A: U(i)"
and
- Coprod_form_cond2: "\<And>i A B. A + B : U(i) \<Longrightarrow> B : U(i)"
+ Coprod_form_cond2: "\<And>i A B. A + B: U(i) \<Longrightarrow> B: U(i)"
lemmas Coprod_rules [intro] = Coprod_form Coprod_intro1 Coprod_intro2
Coprod_elim Coprod_comp1 Coprod_comp2
diff --git a/Equal.thy b/Equal.thy
index 2b49213..8bd7875 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -14,8 +14,8 @@ section \<open>Constants and syntax\<close>
axiomatization
Equal :: "[Term, Term, Term] \<Rightarrow> Term" and
- refl :: "Term \<Rightarrow> Term" ("(refl'(_'))" 1000) and
- indEqual :: "[Term, [Term, Term] \<Rightarrow> Typefam, Term \<Rightarrow> Term, Term, Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>=[_])")
+ refl :: "Term \<Rightarrow> Term" and
+ indEqual :: "[Term \<Rightarrow> Term, Term, Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>=)")
syntax
"_EQUAL" :: "[Term, Term, Term] \<Rightarrow> Term" ("(3_ =\<^sub>_/ _)" [101, 0, 101] 100)
@@ -28,32 +28,32 @@ translations
section \<open>Type rules\<close>
axiomatization where
- Equal_form: "\<And>i A a b. \<lbrakk>A : U(i); a : A; b : A\<rbrakk> \<Longrightarrow> a =\<^sub>A b : U(i)"
+ Equal_form: "\<And>i A a b. \<lbrakk>A: U(i); a: A; b: A\<rbrakk> \<Longrightarrow> a =\<^sub>A b : U(i)"
and
- Equal_intro: "\<And>A a. a : A \<Longrightarrow> refl(a) : a =\<^sub>A a"
+ Equal_intro: "\<And>A a. a : A \<Longrightarrow> refl(a): a =\<^sub>A a"
and
Equal_elim: "\<And>i A C f a b p. \<lbrakk>
- \<And>x y. \<lbrakk>x : A; y : A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U(i);
- \<And>x. x : A \<Longrightarrow> f x : C x x refl(x);
- a : A;
- b : A;
- p : a =\<^sub>A b
- \<rbrakk> \<Longrightarrow> ind\<^sub>=[A] C f a b p : C a b p"
+ \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C(x)(y): x =\<^sub>A y \<longrightarrow> U(i);
+ \<And>x. x: A \<Longrightarrow> f(x) : C(x)(x)(refl x);
+ a: A;
+ b: A;
+ p: a =\<^sub>A b
+ \<rbrakk> \<Longrightarrow> ind\<^sub>=(f)(a)(b)(p) : C(a)(b)(p)"
and
Equal_comp: "\<And>i A C f a. \<lbrakk>
- \<And>x y. \<lbrakk>x : A; y : A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U(i);
- \<And>x. x : A \<Longrightarrow> f x : C x x refl(x);
- a : A
- \<rbrakk> \<Longrightarrow> ind\<^sub>=[A] C f a a refl(a) \<equiv> f a"
+ \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C(x)(y): x =\<^sub>A y \<longrightarrow> U(i);
+ \<And>x. x: A \<Longrightarrow> f(x) : C(x)(x)(refl x);
+ a: A
+ \<rbrakk> \<Longrightarrow> ind\<^sub>=(f)(a)(a)(refl(a)) \<equiv> f(a)"
text "Admissible inference rules for equality type formation:"
axiomatization where
- Equal_form_cond1: "\<And>i A a b. a =\<^sub>A b : U(i) \<Longrightarrow> A : U(i)"
+ Equal_form_cond1: "\<And>i A a b. a =\<^sub>A b: U(i) \<Longrightarrow> A: U(i)"
and
- Equal_form_cond2: "\<And>i A a b. a =\<^sub>A b : U(i) \<Longrightarrow> a : A"
+ Equal_form_cond2: "\<And>i A a b. a =\<^sub>A b: U(i) \<Longrightarrow> a: A"
and
- Equal_form_cond3: "\<And>i A a b. a =\<^sub>A b : U(i) \<Longrightarrow> b : A"
+ Equal_form_cond3: "\<And>i A a b. a =\<^sub>A b: U(i) \<Longrightarrow> b: A"
lemmas Equal_rules [intro] = Equal_form Equal_intro Equal_elim Equal_comp
lemmas Equal_form_conds [intro] = Equal_form_cond1 Equal_form_cond2 Equal_form_cond3
diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index c2bb092..614419e 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -9,10 +9,6 @@ theory HoTT_Base
imports Pure
begin
-text "Use the syntax \<open>f(x)\<close> instead of \<open>f x\<close> for function application."
-
-setup Pure_Thy.old_appl_syntax_setup
-
section \<open>Foundational definitions\<close>
diff --git a/Nat.thy b/Nat.thy
index 93b7a2e..bd2c4ca 100644
--- a/Nat.thy
+++ b/Nat.thy
@@ -14,33 +14,33 @@ axiomatization
Nat :: Term ("\<nat>") and
zero :: Term ("0") and
succ :: "Term \<Rightarrow> Term" and
- indNat :: "[Typefam, [Term, Term] \<Rightarrow> Term, Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>\<nat>)")
+ indNat :: "[[Term, Term] \<Rightarrow> Term, Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>\<nat>)")
where
- Nat_form: "\<nat> : U(O)"
+ Nat_form: "\<nat>: U(O)"
and
- Nat_intro1: "0 : \<nat>"
+ Nat_intro1: "0: \<nat>"
and
- Nat_intro2: "\<And>n. n : \<nat> \<Longrightarrow> succ n : \<nat>"
+ Nat_intro2: "\<And>n. n: \<nat> \<Longrightarrow> succ(n): \<nat>"
and
Nat_elim: "\<And>i C f a n. \<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> C f a n : C n"
+ \<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
Nat_comp1: "\<And>i C f a. \<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
- \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> C f a 0 \<equiv> a"
+ \<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
Nat_comp2: "\<And> i C f a n. \<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> C f a (succ n) \<equiv> f n (ind\<^sub>\<nat> C f a n)"
+ \<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)"
lemmas Nat_rules [intro] = Nat_form Nat_intro1 Nat_intro2 Nat_elim Nat_comp1 Nat_comp2
lemmas Nat_comps [comp] = Nat_comp1 Nat_comp2
diff --git a/Prod.thy b/Prod.thy
index 845de4b..01cd006 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -27,10 +27,10 @@ syntax
text "The translations below bind the variable \<open>x\<close> in the expressions \<open>B\<close> and \<open>b\<close>."
translations
- "\<Prod>x:A. B" \<rightleftharpoons> "CONST Prod(A, \<lambda>x. B)"
- "\<^bold>\<lambda>x:A. b" \<rightleftharpoons> "CONST lambda(A, \<lambda>x. b)"
- "PROD x:A. B" \<rightharpoonup> "CONST Prod(A, \<lambda>x. B)"
- "%%x:A. b" \<rightharpoonup> "CONST lambda(A, \<lambda>x. b)"
+ "\<Prod>x:A. B" \<rightleftharpoons> "CONST Prod A (\<lambda>x. B)"
+ "\<^bold>\<lambda>x:A. b" \<rightleftharpoons> "CONST lambda A (\<lambda>x. b)"
+ "PROD x:A. B" \<rightharpoonup> "CONST Prod A (\<lambda>x. B)"
+ "%%x:A. b" \<rightharpoonup> "CONST lambda A (\<lambda>x. b)"
text "Nondependent functions are a special case."
@@ -84,9 +84,9 @@ where
and
Unit_intro: "\<star>: \<one>"
and
- Unit_elim: "\<And>i C c a. \<lbrakk>C: \<one> \<longrightarrow> U(i); c: C(\<star>); a: \<one>\<rbrakk> \<Longrightarrow> ind\<^sub>\<one>(c, a) : C(a)"
+ Unit_elim: "\<And>i C c a. \<lbrakk>C: \<one> \<longrightarrow> U(i); c: C(\<star>); a: \<one>\<rbrakk> \<Longrightarrow> ind\<^sub>\<one>(c)(a) : C(a)"
and
- Unit_comp: "\<And>i C c. \<lbrakk>C: \<one> \<longrightarrow> U(i); c: C(\<star>)\<rbrakk> \<Longrightarrow> ind\<^sub>\<one>(c, \<star>) \<equiv> c"
+ Unit_comp: "\<And>i C c. \<lbrakk>C: \<one> \<longrightarrow> U(i); c: C(\<star>)\<rbrakk> \<Longrightarrow> ind\<^sub>\<one>(c)(\<star>) \<equiv> c"
lemmas Unit_rules [intro] = Unit_form Unit_intro Unit_elim Unit_comp
lemmas Unit_comps [comp] = Unit_comp
diff --git a/Sum.thy b/Sum.thy
index 2d6e64b..cdfe5bd 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -22,8 +22,8 @@ syntax
"_SUM_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term" ("(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)"
+ "\<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."
@@ -40,25 +40,25 @@ and
and
Sum_elim: "\<And>i A B C f p. \<lbrakk>
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));
+ \<And>x y. \<lbrakk>x: A; y: B(x)\<rbrakk> \<Longrightarrow> f(x)(y) : C((x,y));
p : \<Sum>x:A. B(x)
- \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum>(f, p) : C(p)" (* What does writing \<lambda>x y. f(x, y) change? *)
+ \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum>(f)(p) : C(p)" (* What does writing \<lambda>x y. f(x, y) change? *)
and
Sum_comp: "\<And>i A B C f a b. \<lbrakk>
- A : U(i);
+ A: U(i);
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);
- a : A;
- b : B a
- \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum>[A,B] C f (a,b) \<equiv> f a b"
+ 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));
+ a: A;
+ b: B(a)
+ \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum>(f)((a,b)) \<equiv> f(a)(b)"
text "Admissible inference rules for sum formation:"
axiomatization where
- Sum_form_cond1: "\<And>i A B. (\<Sum>x:A. B x : U(i)) \<Longrightarrow> A : U(i)"
+ Sum_form_cond1: "\<And>i A B. (\<Sum>x:A. B(x): U(i)) \<Longrightarrow> A: U(i)"
and
- Sum_form_cond2: "\<And>i A B. (\<Sum>x:A. B x : U(i)) \<Longrightarrow> B: A \<longrightarrow> U(i)"
+ Sum_form_cond2: "\<And>i A B. (\<Sum>x:A. B(x): U(i)) \<Longrightarrow> B: A \<longrightarrow> U(i)"
lemmas Sum_rules [intro] = Sum_form Sum_intro Sum_elim Sum_comp
lemmas Sum_form_conds [intro (*elim, wellform*)] = Sum_form_cond1 Sum_form_cond2
@@ -69,11 +69,11 @@ section \<open>Empty type\<close>
axiomatization
Empty :: Term ("\<zero>") and
- indEmpty :: "[Typefam, Term] \<Rightarrow> Term" ("(1ind\<^sub>\<zero>)")
+ indEmpty :: "Term \<Rightarrow> Term" ("(1ind\<^sub>\<zero>)")
where
Empty_form: "\<zero> : U(O)"
and
- Empty_elim: "\<And>i C z. \<lbrakk>C: \<zero> \<longrightarrow> U(i); z : \<zero>\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero> C z : C z"
+ Empty_elim: "\<And>i C z. \<lbrakk>C: \<zero> \<longrightarrow> U(i); z: \<zero>\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero>(z): C(z)"
lemmas Empty_rules [intro] = Empty_form Empty_elim
diff --git a/scratch.thy b/scratch.thy
index b88a8fc..55e7023 100644
--- a/scratch.thy
+++ b/scratch.thy
@@ -3,9 +3,9 @@ theory scratch
begin
-abbreviation pred where "pred \<equiv> \<^bold>\<lambda>n:\<nat>. (ind\<^sub>\<nat> (\<lambda>n. \<nat>) (\<lambda>n c. n) 0 n)"
+abbreviation pred where "pred \<equiv> \<^bold>\<lambda>n:\<nat>. ind\<^sub>\<nat>(\<lambda>n c. n, 0, n)"
-schematic_goal "?a : (pred`0) =\<^sub>\<nat> 0"
+schematic_goal "?a: (pred`0) =\<^sub>\<nat> 0"
apply (subst comp)
apply (rule Nat_form)
prefer 4 apply (subst comp)
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-28 23:40:41 +0000