Non-annotated object lambda

8 files changed, 78 insertions, 56 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"
diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index ed21934..1ca027f 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -15,24 +15,37 @@ keywords
 begin
 
 
-section \<open>Preamble\<close>
+section \<open>Prelude\<close>
 
 declare [[eta_contract=false]]
 
+setup \<open>
+let
+  val typ = Simple_Syntax.read_typ
+  fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range)
+in
+  Sign.del_syntax (Print_Mode.ASCII, true)
+    [("_lambda", typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic", mixfix ("(3fn _./ _)", [0, 3], 3))]
+  #> Sign.del_syntax Syntax.mode_default
+    [("_lambda", typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic", mixfix ("(3\<lambda>_./ _)", [0, 3], 3))]
+  #> Sign.add_syntax Syntax.mode_default
+    [("_lambda", typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic", mixfix ("(3fn _./ _)", [0, 3], 3))]
+end
+\<close>
+
 syntax "_dollar" :: \<open>logic \<Rightarrow> logic \<Rightarrow> logic\<close> (infixr "$" 3)
 translations "a $ b" \<rightharpoonup> "a (b)"
 
-abbreviation (input) K where "K x \<equiv> \<lambda>_. x"
-
-
-section \<open>Metatype setup\<close>
+abbreviation (input) K where "K x \<equiv> fn _. x"
 
 typedecl o
 
+judgment has_type :: \<open>o \<Rightarrow> o \<Rightarrow> prop\<close> ("(2_:/ _)" 999)
 
-section \<open>Judgments\<close>
 
-judgment has_type :: \<open>o \<Rightarrow> o \<Rightarrow> prop\<close> ("(2_:/ _)" 999)
+section \<open>Type annotations\<close>
+
+consts anno :: \<open>o \<Rightarrow> o \<Rightarrow> o\<close> ("'(_: _')")
 
 
 section \<open>Universes\<close>
@@ -74,15 +87,15 @@ syntax
   "_lam"  :: \<open>idts \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> ("(2\<lambda>_: _./ _)" 30)
   "_lam2" :: \<open>idts \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close>
 translations
-  "\<Prod>x xs: A. B" \<rightharpoonup> "CONST Pi A (\<lambda>x. _Pi2 xs A B)"
-  "_Pi2 x A B" \<rightharpoonup> "\<Prod>x: A. B"
-  "\<Prod>x: A. B"    \<rightleftharpoons> "CONST Pi A (\<lambda>x. B)"
-  "\<lambda>x xs: A. b" \<rightharpoonup> "CONST lam A (\<lambda>x. _lam2 xs A b)"
+  "\<Prod>x xs: A. B" \<rightharpoonup> "CONST Pi A (fn x. _Pi2 xs A B)"
+  "_Pi2 x A B"  \<rightharpoonup> "\<Prod>x: A. B"
+  "\<Prod>x: A. B"    \<rightleftharpoons> "CONST Pi A (fn x. B)"
+  "\<lambda>x xs: A. b" \<rightharpoonup> "CONST lam A (fn x. _lam2 xs A b)"
   "_lam2 x A b" \<rightharpoonup> "\<lambda>x: A. b"
-  "\<lambda>x: A. b"    \<rightleftharpoons> "CONST lam A (\<lambda>x. b)"
+  "\<lambda>x: A. b"    \<rightleftharpoons> "CONST lam A (fn x. b)"
 
 abbreviation Fn (infixr "\<rightarrow>" 40) where "A \<rightarrow> B \<equiv> \<Prod>_: A. B"
-
+term "\<lambda>x: A. b x"
 axiomatization where
   PiF: "\<lbrakk>\<And>x. x: A \<Longrightarrow> B x: U i; A: U i\<rbrakk> \<Longrightarrow> \<Prod>x: A. B x: U i" and
 
@@ -113,7 +126,7 @@ axiomatization
 
 syntax "_Sum" :: \<open>idt \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> ("(2\<Sum>_: _./ _)" 20)
 
-translations "\<Sum>x: A. B" \<rightleftharpoons> "CONST Sig A (\<lambda>x. B)"
+translations "\<Sum>x: A. B" \<rightleftharpoons> "CONST Sig A (fn x. B)"
 
 abbreviation Prod (infixl "\<times>" 60)
   where "A \<times> B \<equiv> \<Sum>_: A. B"
@@ -132,7 +145,7 @@ axiomatization where
     \<And>x. x : A \<Longrightarrow> B x: U i;
     \<And>x y. \<lbrakk>x: A; y: B x\<rbrakk> \<Longrightarrow> f x y: C <x, y>;
     \<And>p. p: \<Sum>x: A. B x \<Longrightarrow> C p: U i
-    \<rbrakk> \<Longrightarrow> SigInd A (\<lambda>x. B x) (\<lambda>p. C p) f p: C p" and
+    \<rbrakk> \<Longrightarrow> SigInd A (fn x. B x) (fn p. C p) f p: C p" and
 
   Sig_comp: "\<lbrakk>
     a: A;
@@ -140,7 +153,7 @@ axiomatization where
     \<And>x. x: A \<Longrightarrow> B x: U i;
     \<And>p. p: \<Sum>x: A. B x \<Longrightarrow> C p: U i;
     \<And>x y. \<lbrakk>x: A; y: B x\<rbrakk> \<Longrightarrow> f x y: C <x, y>
-    \<rbrakk> \<Longrightarrow> SigInd A (\<lambda>x. B x) (\<lambda>p. C p) f <a, b> \<equiv> f a b" and
+    \<rbrakk> \<Longrightarrow> SigInd A (fn x. B x) (fn p. C p) f <a, b> \<equiv> f a b" and
 
   Sig_cong: "\<lbrakk>
     \<And>x. x: A \<Longrightarrow> B x \<equiv> B' x;
@@ -249,7 +262,7 @@ consts rewrite_HOLE :: "'a::{}"  ("\<hole>")
 
 lemma eta_expand:
   fixes f :: "'a::{} \<Rightarrow> 'b::{}"
-  shows "f \<equiv> \<lambda>x. f x" .
+  shows "f \<equiv> fn x. f x" .
 
 lemma rewr_imp:
   assumes "PROP A \<equiv> PROP B"
@@ -301,11 +314,23 @@ text \<open>Automatically insert inhabitation judgments where needed:\<close>
 syntax inhabited :: \<open>o \<Rightarrow> prop\<close> ("(_)")
 translations "inhabited A" \<rightharpoonup> "CONST has_type {} A"
 
+text \<open>Implicit lambdas\<close>
+
+definition lam_i where [implicit]: "lam_i f \<equiv> lam ? f"
+
+syntax
+  "_lam_i"  :: \<open>idts \<Rightarrow> o \<Rightarrow> o\<close> ("(2\<lambda>_./ _)" 30)
+  "_lam_i2" :: \<open>idts \<Rightarrow> o \<Rightarrow> o\<close>
+translations
+  "\<lambda>x xs. b" \<rightharpoonup> "CONST lam_i (fn x. _lam_i2 xs b)"
+  "_lam_i2 x b" \<rightharpoonup> "\<lambda>x. b"
+  "\<lambda>x. b"    \<rightleftharpoons> "CONST lam_i (fn x. b)"
+
 subsection \<open>Lambda coercion\<close>
 
 \<comment> \<open>Coerce object lambdas to meta-lambdas\<close>
 abbreviation (input) lambda :: \<open>o \<Rightarrow> o \<Rightarrow> o\<close>
-  where "lambda f \<equiv> \<lambda>x. f `x"
+  where "lambda f \<equiv> fn x. f `x"
 
 ML_file \<open>~~/src/Tools/subtyping.ML\<close>
 declare [[coercion_enabled, coercion lambda]]
@@ -409,8 +434,8 @@ lemma id_U [typechk]:
 
 section \<open>Pairs\<close>
 
-definition "fst A B \<equiv> \<lambda>p: \<Sum>x: A. B x. SigInd A B (\<lambda>_. A) (\<lambda>x y. x) p"
-definition "snd A B \<equiv> \<lambda>p: \<Sum>x: A. B x. SigInd A B (\<lambda>p. B (fst A B p)) (\<lambda>x y. y) p"
+definition "fst A B \<equiv> \<lambda>p: \<Sum>x: A. B x. SigInd A B (fn _. A) (fn x y. x) p"
+definition "snd A B \<equiv> \<lambda>p: \<Sum>x: A. B x. SigInd A B (fn p. B (fst A B p)) (fn x y. y) p"
 
 lemma fst_type [typechk]:
   assumes "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i"
diff --git a/spartan/lib/List.thy b/spartan/lib/List.thy
index 11b8406..a755859 100644
--- a/spartan/lib/List.thy
+++ b/spartan/lib/List.thy
@@ -26,13 +26,13 @@ where
     c\<^sub>0: C (nil A);
     \<And>x xs rec. \<lbrakk>x: A; xs: List A; rec: C xs\<rbrakk> \<Longrightarrow> f x xs rec: C (cons A x xs);
     \<And>xs. xs: List A \<Longrightarrow> C xs: U i
-    \<rbrakk> \<Longrightarrow> ListInd A (\<lambda>xs. C xs) c\<^sub>0 (\<lambda>x xs rec. f x xs rec) xs: C xs" and
+    \<rbrakk> \<Longrightarrow> ListInd A (fn xs. C xs) c\<^sub>0 (fn x xs rec. f x xs rec) xs: C xs" and
 
   List_comp_nil: "\<lbrakk>
     c\<^sub>0: C (nil A);
     \<And>x xs rec. \<lbrakk>x: A; xs: List A; rec: C xs\<rbrakk> \<Longrightarrow> f x xs rec: C (cons A x xs);
     \<And>xs. xs: List A \<Longrightarrow> C xs: U i
-    \<rbrakk> \<Longrightarrow> ListInd A (\<lambda>xs. C xs) c\<^sub>0 (\<lambda>x xs rec. f x xs rec) (nil A) \<equiv> c\<^sub>0" and
+    \<rbrakk> \<Longrightarrow> ListInd A (fn xs. C xs) c\<^sub>0 (fn x xs rec. f x xs rec) (nil A) \<equiv> c\<^sub>0" and
 
   List_comp_cons: "\<lbrakk>
     xs: List A;
@@ -40,15 +40,15 @@ where
     \<And>x xs rec. \<lbrakk>x: A; xs: List A; rec: C xs\<rbrakk> \<Longrightarrow> f x xs rec: C (cons A x xs);
     \<And>xs. xs: List A \<Longrightarrow> C xs: U i
     \<rbrakk> \<Longrightarrow>
-      ListInd A (\<lambda>xs. C xs) c\<^sub>0 (\<lambda>x xs rec. f x xs rec) (cons A x xs) \<equiv>
-        f x xs (ListInd A (\<lambda>xs. C xs) c\<^sub>0 (\<lambda>x xs rec. f x xs rec) xs)"
+      ListInd A (fn xs. C xs) c\<^sub>0 (fn x xs rec. f x xs rec) (cons A x xs) \<equiv>
+        f x xs (ListInd A (fn xs. C xs) c\<^sub>0 (fn x xs rec. f x xs rec) xs)"
 
 lemmas
   [intros] = ListF List_nil List_cons and
   [elims "?xs"] = ListE and
   [comps] = List_comp_nil List_comp_cons
 
-abbreviation "ListRec A C \<equiv> ListInd A (\<lambda>_. C)"
+abbreviation "ListRec A C \<equiv> ListInd A (fn _. C)"
 
 Lemma list_cases [cases]:
   assumes
@@ -56,7 +56,7 @@ Lemma list_cases [cases]:
     nil_case: "c\<^sub>0: C (nil A)" and
     cons_case: "\<And>x xs. \<lbrakk>x: A; xs: List A\<rbrakk> \<Longrightarrow> f x xs: C (cons A x xs)" and
     "\<And>xs. xs: List A \<Longrightarrow> C xs: U i"
-  shows "?List_cases A (\<lambda>xs. C xs) c\<^sub>0 (\<lambda>x xs. f x xs) xs: C xs"
+  shows "C xs"
   by (elim xs) (fact nil_case, rule cons_case)
 
 
diff --git a/spartan/lib/Maybe.thy b/spartan/lib/Maybe.thy
index 6729812..d821920 100644
--- a/spartan/lib/Maybe.thy
+++ b/spartan/lib/Maybe.thy
@@ -24,7 +24,7 @@ Definition MaybeInd:
     "c\<^sub>0: C (none A)"
     "\<And>a. a: A \<Longrightarrow> f a: C (some A a)"
     "m: Maybe A"
-  shows "?MaybeInd A (\<lambda>m. C m) c\<^sub>0 (\<lambda>a. f a) m: C m"
+  shows "C m"
   supply assms[unfolded Maybe_def none_def some_def]
   apply (elim m)
   \<guillemotright> unfolding Maybe_def .
@@ -38,7 +38,7 @@ Lemma Maybe_comp_none:
     "c\<^sub>0: C (none A)"
     "\<And>a. a: A \<Longrightarrow> f a: C (some A a)"
     "\<And>m. m: Maybe A \<Longrightarrow> C m: U i"
-  shows "MaybeInd A (\<lambda>m. C m) c\<^sub>0 (\<lambda>a. f a) (none A) \<equiv> c\<^sub>0"
+  shows "MaybeInd A C c\<^sub>0 f (none A) \<equiv> c\<^sub>0"
   supply assms[unfolded Maybe_def some_def none_def]
   unfolding MaybeInd_def none_def by reduce
 
@@ -49,7 +49,7 @@ Lemma Maybe_comp_some:
     "c\<^sub>0: C (none A)"
     "\<And>a. a: A \<Longrightarrow> f a: C (some A a)"
     "\<And>m. m: Maybe A \<Longrightarrow> C m: U i"
-  shows "MaybeInd A (\<lambda>m. C m) c\<^sub>0 (\<lambda>a. f a) (some A a) \<equiv> f a"
+  shows "MaybeInd A C c\<^sub>0 f (some A a) \<equiv> f a"
   supply assms[unfolded Maybe_def some_def none_def]
   unfolding MaybeInd_def some_def by (reduce add: Maybe_def)
 
@@ -62,11 +62,8 @@ lemmas
 
 abbreviation "MaybeRec A C \<equiv> MaybeInd A (K C)"
 
-definition none_i ("none")
-  where [implicit]: "none \<equiv> Maybe.none ?"
-
-definition some_i ("some")
-  where [implicit]: "some a \<equiv> Maybe.some ? a"
+definition none_i ("none") where [implicit]: "none \<equiv> Maybe.none ?"
+definition some_i ("some") where [implicit]: "some a \<equiv> Maybe.some ? a"
 
 translations
   "none" \<leftharpoondown> "CONST Maybe.none A"
diff --git a/spartan/lib/More_Types.thy b/spartan/lib/More_Types.thy
index 38ba2aa..0d7096f 100644
--- a/spartan/lib/More_Types.thy
+++ b/spartan/lib/More_Types.thy
@@ -25,21 +25,21 @@ axiomatization where
     \<And>s. s: A \<or> B \<Longrightarrow> C s: U i;
     \<And>a. a: A \<Longrightarrow> c a: C (inl A B a);
     \<And>b. b: B \<Longrightarrow> d b: C (inr A B b)
-    \<rbrakk> \<Longrightarrow> SumInd A B (\<lambda>s. C s) (\<lambda>a. c a) (\<lambda>b. d b) s: C s" and
+    \<rbrakk> \<Longrightarrow> SumInd A B (fn s. C s) (fn a. c a) (fn b. d b) s: C s" and
 
   Sum_comp_inl: "\<lbrakk>
     a: A;
     \<And>s. s: A \<or> B \<Longrightarrow> C s: U i;
     \<And>a. a: A \<Longrightarrow> c a: C (inl A B a);
     \<And>b. b: B \<Longrightarrow> d b: C (inr A B b)
-    \<rbrakk> \<Longrightarrow> SumInd A B (\<lambda>s. C s) (\<lambda>a. c a) (\<lambda>b. d b) (inl A B a) \<equiv> c a" and
+    \<rbrakk> \<Longrightarrow> SumInd A B (fn s. C s) (fn a. c a) (fn b. d b) (inl A B a) \<equiv> c a" and
 
   Sum_comp_inr: "\<lbrakk>
     b: B;
     \<And>s. s: A \<or> B \<Longrightarrow> C s: U i;
     \<And>a. a: A \<Longrightarrow> c a: C (inl A B a);
     \<And>b. b: B \<Longrightarrow> d b: C (inr A B b)
-    \<rbrakk> \<Longrightarrow> SumInd A B (\<lambda>s. C s) (\<lambda>a. c a) (\<lambda>b. d b) (inr A B b) \<equiv> d b"
+    \<rbrakk> \<Longrightarrow> SumInd A B (fn s. C s) (fn a. c a) (fn b. d b) (inr A B b) \<equiv> d b"
 
 lemmas
   [intros] = SumF Sum_inl Sum_inr and
@@ -67,13 +67,13 @@ axiomatization where
 
   TopI: "tt: \<top>" and
 
-  TopE: "\<lbrakk>a: \<top>; \<And>x. x: \<top> \<Longrightarrow> C x: U i; c: C tt\<rbrakk> \<Longrightarrow> TopInd (\<lambda>x. C x) c a: C a" and
+  TopE: "\<lbrakk>a: \<top>; \<And>x. x: \<top> \<Longrightarrow> C x: U i; c: C tt\<rbrakk> \<Longrightarrow> TopInd (fn x. C x) c a: C a" and
 
-  Top_comp: "\<lbrakk>\<And>x. x: \<top> \<Longrightarrow> C x: U i; c: C tt\<rbrakk> \<Longrightarrow> TopInd (\<lambda>x. C x) c tt \<equiv> c"
+  Top_comp: "\<lbrakk>\<And>x. x: \<top> \<Longrightarrow> C x: U i; c: C tt\<rbrakk> \<Longrightarrow> TopInd (fn x. C x) c tt \<equiv> c"
 and
   BotF: "\<bottom>: U i" and
 
-  BotE: "\<lbrakk>x: \<bottom>; \<And>x. x: \<bottom> \<Longrightarrow> C x: U i\<rbrakk> \<Longrightarrow> BotInd (\<lambda>x. C x) x: C x"
+  BotE: "\<lbrakk>x: \<bottom>; \<And>x. x: \<bottom> \<Longrightarrow> C x: U i\<rbrakk> \<Longrightarrow> BotInd (fn x. C x) x: C x"
 
 lemmas
   [intros] = TopF TopI BotF and