diff options
Diffstat (limited to 'hott')
| -rw-r--r-- | hott/Equivalence.thy | 12 | ||||
| -rw-r--r-- | hott/Identity.thy | 8 | ||||
| -rw-r--r-- | hott/More_List.thy | 2 | ||||
| -rw-r--r-- | hott/Nat.thy | 10 |
4 files changed, 16 insertions, 16 deletions
diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy index face775..66248a9 100644 --- a/hott/Equivalence.thy +++ b/hott/Equivalence.thy @@ -73,7 +73,7 @@ Lemma (derive) commute_homotopy: "x: A" "y: A" "p: x =\<^bsub>A\<^esub> y" "f: A \<rightarrow> B" "g: A \<rightarrow> B" - "H: homotopy A (\<lambda>_. B) f g" + "H: homotopy A (fn _. B) f g" shows "(H x) \<bullet> g[p] = f[p] \<bullet> (H y)" \<comment> \<open>Need this assumption unfolded for typechecking\<close> supply assms(8)[unfolded homotopy_def] @@ -94,7 +94,7 @@ Corollary (derive) commute_homotopy': "A: U i" "x: A" "f: A \<rightarrow> A" - "H: homotopy A (\<lambda>_. A) f (id A)" + "H: homotopy A (fn _. A) f (id A)" shows "H (f x) = f [H x]" oops @@ -125,7 +125,7 @@ Lemma homotopy_funcomp_left: Lemma homotopy_funcomp_right: assumes - "H: homotopy A (\<lambda>_. B) f f'" + "H: homotopy A (fn _. B) f f'" "f: A \<rightarrow> B" "f': A \<rightarrow> B" "g: B \<rightarrow> C" @@ -149,7 +149,7 @@ section \<open>Quasi-inverse and bi-invertibility\<close> subsection \<open>Quasi-inverses\<close> definition "qinv A B f \<equiv> \<Sum>g: B \<rightarrow> A. - homotopy A (\<lambda>_. A) (g \<circ>\<^bsub>A\<^esub> f) (id A) \<times> homotopy B (\<lambda>_. B) (f \<circ>\<^bsub>B\<^esub> g) (id B)" + homotopy A (fn _. A) (g \<circ>\<^bsub>A\<^esub> f) (id A) \<times> homotopy B (fn _. B) (f \<circ>\<^bsub>B\<^esub> g) (id B)" lemma qinv_type [typechk]: assumes "A: U i" "B: U i" "f: A \<rightarrow> B" @@ -210,8 +210,8 @@ Lemma (derive) funcomp_qinv: subsection \<open>Bi-invertible maps\<close> definition "biinv A B f \<equiv> - (\<Sum>g: B \<rightarrow> A. homotopy A (\<lambda>_. A) (g \<circ>\<^bsub>A\<^esub> f) (id A)) - \<times> (\<Sum>g: B \<rightarrow> A. homotopy B (\<lambda>_. B) (f \<circ>\<^bsub>B\<^esub> g) (id B))" + (\<Sum>g: B \<rightarrow> A. homotopy A (fn _. A) (g \<circ>\<^bsub>A\<^esub> f) (id A)) + \<times> (\<Sum>g: B \<rightarrow> A. homotopy B (fn _. B) (f \<circ>\<^bsub>B\<^esub> g) (id B))" lemma biinv_type [typechk]: assumes "A: U i" "B: U i" "f: A \<rightarrow> B" diff --git a/hott/Identity.thy b/hott/Identity.thy index 308e664..dd2d6a0 100644 --- a/hott/Identity.thy +++ b/hott/Identity.thy @@ -30,13 +30,13 @@ axiomatization where b: A; \<And>x y p. \<lbrakk>p: x =\<^bsub>A\<^esub> y; x: A; y: A\<rbrakk> \<Longrightarrow> C x y p: U i; \<And>x. x: A \<Longrightarrow> f x: C x x (refl x) - \<rbrakk> \<Longrightarrow> IdInd A (\<lambda>x y p. C x y p) (\<lambda>x. f x) a b p: C a b p" and + \<rbrakk> \<Longrightarrow> IdInd A (fn x y p. C x y p) (fn x. f x) a b p: C a b p" and Id_comp: "\<lbrakk> a: A; \<And>x y p. \<lbrakk>x: A; y: A; p: x =\<^bsub>A\<^esub> y\<rbrakk> \<Longrightarrow> C x y p: U i; \<And>x. x: A \<Longrightarrow> f x: C x x (refl x) - \<rbrakk> \<Longrightarrow> IdInd A (\<lambda>x y p. C x y p) (\<lambda>x. f x) a a (refl a) \<equiv> f a" + \<rbrakk> \<Longrightarrow> IdInd A (fn x y p. C x y p) (fn x. f x) a a (refl a) \<equiv> f a" lemmas [intros] = IdF IdI and @@ -347,7 +347,7 @@ Lemma (derive) transport_compose_typefam: "x: A" "y: A" "p: x =\<^bsub>A\<^esub> y" "u: P (f x)" - shows "trans (\<lambda>x. P (f x)) p u = trans P f[p] u" + shows "trans (fn x. P (f x)) p u = trans P f[p] u" by (eq p) (reduce; intros) Lemma (derive) transport_function_family: @@ -367,7 +367,7 @@ Lemma (derive) transport_const: "A: U i" "B: U i" "x: A" "y: A" "p: x =\<^bsub>A\<^esub> y" - shows "\<Prod>b: B. trans (\<lambda>_. B) p b = b" + shows "\<Prod>b: B. trans (fn _. B) p b = b" by (intro, eq p) (reduce; intro) definition transport_const_i ("trans'_const") diff --git a/hott/More_List.thy b/hott/More_List.thy index a216987..460dc7b 100644 --- a/hott/More_List.thy +++ b/hott/More_List.thy @@ -7,7 +7,7 @@ begin section \<open>Length\<close> -definition [implicit]: "len \<equiv> ListRec ? Nat 0 (\<lambda>_ _ rec. suc rec)" +definition [implicit]: "len \<equiv> ListRec ? Nat 0 (fn _ _ rec. suc rec)" experiment begin Lemma "len [] \<equiv> ?n" by (subst comps)+ diff --git a/hott/Nat.thy b/hott/Nat.thy index 50b7996..4abd315 100644 --- a/hott/Nat.thy +++ b/hott/Nat.thy @@ -20,13 +20,13 @@ where c\<^sub>0: C 0; \<And>k rec. \<lbrakk>k: Nat; rec: C k\<rbrakk> \<Longrightarrow> f k rec: C (suc k); \<And>n. n: Nat \<Longrightarrow> C n: U i - \<rbrakk> \<Longrightarrow> NatInd (\<lambda>n. C n) c\<^sub>0 (\<lambda>k rec. f k rec) n: C n" and + \<rbrakk> \<Longrightarrow> NatInd (fn n. C n) c\<^sub>0 (fn k rec. f k rec) n: C n" and Nat_comp_zero: "\<lbrakk> c\<^sub>0: C 0; \<And>k rec. \<lbrakk>k: Nat; rec: C k\<rbrakk> \<Longrightarrow> f k rec: C (suc k); \<And>n. n: Nat \<Longrightarrow> C n: U i - \<rbrakk> \<Longrightarrow> NatInd (\<lambda>n. C n) c\<^sub>0 (\<lambda>k rec. f k rec) 0 \<equiv> c\<^sub>0" and + \<rbrakk> \<Longrightarrow> NatInd (fn n. C n) c\<^sub>0 (fn k rec. f k rec) 0 \<equiv> c\<^sub>0" and Nat_comp_suc: "\<lbrakk> n: Nat; @@ -34,15 +34,15 @@ where \<And>k rec. \<lbrakk>k: Nat; rec: C k\<rbrakk> \<Longrightarrow> f k rec: C (suc k); \<And>n. n: Nat \<Longrightarrow> C n: U i \<rbrakk> \<Longrightarrow> - NatInd (\<lambda>n. C n) c\<^sub>0 (\<lambda>k rec. f k rec) (suc n) \<equiv> - f n (NatInd (\<lambda>n. C n) c\<^sub>0 (\<lambda>k rec. f k rec) n)" + NatInd (fn n. C n) c\<^sub>0 (fn k rec. f k rec) (suc n) \<equiv> + f n (NatInd (fn n. C n) c\<^sub>0 (fn k rec. f k rec) n)" lemmas [intros] = NatF Nat_zero Nat_suc and [elims "?n"] = NatE and [comps] = Nat_comp_zero Nat_comp_suc -abbreviation "NatRec C \<equiv> NatInd (\<lambda>_. C)" +abbreviation "NatRec C \<equiv> NatInd (fn _. C)" abbreviation one ("1") where "1 \<equiv> suc 0" abbreviation two ("2") where "2 \<equiv> suc 1" |