Non-annotated object lambda

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"