From 831f33468f227c0dc96bd31380236f2c77e70c52 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Thu, 9 Jul 2020 13:35:39 +0200 Subject: Non-annotated object lambda --- hott/Equivalence.thy | 12 ++++++------ hott/Identity.thy | 8 ++++---- hott/More_List.thy | 2 +- hott/Nat.thy | 10 +++++----- 4 files changed, 16 insertions(+), 16 deletions(-) (limited to 'hott') 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 \ B" "g: A \ B" - "H: homotopy A (\_. B) f g" + "H: homotopy A (fn _. B) f g" shows "(H x) \ g[p] = f[p] \ (H y)" \ \Need this assumption unfolded for typechecking\ supply assms(8)[unfolded homotopy_def] @@ -94,7 +94,7 @@ Corollary (derive) commute_homotopy': "A: U i" "x: A" "f: A \ A" - "H: homotopy A (\_. 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 (\_. B) f f'" + "H: homotopy A (fn _. B) f f'" "f: A \ B" "f': A \ B" "g: B \ C" @@ -149,7 +149,7 @@ section \Quasi-inverse and bi-invertibility\ subsection \Quasi-inverses\ definition "qinv A B f \ \g: B \ A. - homotopy A (\_. A) (g \\<^bsub>A\<^esub> f) (id A) \ homotopy B (\_. B) (f \\<^bsub>B\<^esub> g) (id B)" + homotopy A (fn _. A) (g \\<^bsub>A\<^esub> f) (id A) \ homotopy B (fn _. B) (f \\<^bsub>B\<^esub> g) (id B)" lemma qinv_type [typechk]: assumes "A: U i" "B: U i" "f: A \ B" @@ -210,8 +210,8 @@ Lemma (derive) funcomp_qinv: subsection \Bi-invertible maps\ definition "biinv A B f \ - (\g: B \ A. homotopy A (\_. A) (g \\<^bsub>A\<^esub> f) (id A)) - \ (\g: B \ A. homotopy B (\_. B) (f \\<^bsub>B\<^esub> g) (id B))" + (\g: B \ A. homotopy A (fn _. A) (g \\<^bsub>A\<^esub> f) (id A)) + \ (\g: B \ A. homotopy B (fn _. B) (f \\<^bsub>B\<^esub> g) (id B))" lemma biinv_type [typechk]: assumes "A: U i" "B: U i" "f: A \ 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; \x y p. \p: x =\<^bsub>A\<^esub> y; x: A; y: A\ \ C x y p: U i; \x. x: A \ f x: C x x (refl x) - \ \ IdInd A (\x y p. C x y p) (\x. f x) a b p: C a b p" and + \ \ IdInd A (fn x y p. C x y p) (fn x. f x) a b p: C a b p" and Id_comp: "\ a: A; \x y p. \x: A; y: A; p: x =\<^bsub>A\<^esub> y\ \ C x y p: U i; \x. x: A \ f x: C x x (refl x) - \ \ IdInd A (\x y p. C x y p) (\x. f x) a a (refl a) \ f a" + \ \ IdInd A (fn x y p. C x y p) (fn x. f x) a a (refl a) \ 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 (\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 "\b: B. trans (\_. B) p b = b" + shows "\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 \Length\ -definition [implicit]: "len \ ListRec ? Nat 0 (\_ _ rec. suc rec)" +definition [implicit]: "len \ ListRec ? Nat 0 (fn _ _ rec. suc rec)" experiment begin Lemma "len [] \ ?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; \k rec. \k: Nat; rec: C k\ \ f k rec: C (suc k); \n. n: Nat \ C n: U i - \ \ NatInd (\n. C n) c\<^sub>0 (\k rec. f k rec) n: C n" and + \ \ NatInd (fn n. C n) c\<^sub>0 (fn k rec. f k rec) n: C n" and Nat_comp_zero: "\ c\<^sub>0: C 0; \k rec. \k: Nat; rec: C k\ \ f k rec: C (suc k); \n. n: Nat \ C n: U i - \ \ NatInd (\n. C n) c\<^sub>0 (\k rec. f k rec) 0 \ c\<^sub>0" and + \ \ NatInd (fn n. C n) c\<^sub>0 (fn k rec. f k rec) 0 \ c\<^sub>0" and Nat_comp_suc: "\ n: Nat; @@ -34,15 +34,15 @@ where \k rec. \k: Nat; rec: C k\ \ f k rec: C (suc k); \n. n: Nat \ C n: U i \ \ - NatInd (\n. C n) c\<^sub>0 (\k rec. f k rec) (suc n) \ - f n (NatInd (\n. C n) c\<^sub>0 (\k rec. f k rec) n)" + NatInd (fn n. C n) c\<^sub>0 (fn k rec. f k rec) (suc n) \ + 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 \ NatInd (\_. C)" +abbreviation "NatRec C \ NatInd (fn _. C)" abbreviation one ("1") where "1 \ suc 0" abbreviation two ("2") where "2 \ suc 1" -- cgit v1.2.3