diff options
| author | Josh Chen | 2020-07-09 13:35:39 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-07-09 13:35:39 +0200 |
| commit | 831f33468f227c0dc96bd31380236f2c77e70c52 (patch) | |
| tree | 5fa4718dc7a902a84ddb0e50750e962755f81b79 /hott/Identity.thy | |
| parent | fc9ba2141aefa685bacc47a9c2eab2cc718d8620 (diff) | |
Non-annotated object lambda
Diffstat (limited to 'hott/Identity.thy')
| -rw-r--r-- | hott/Identity.thy | 8 |
1 files changed, 4 insertions, 4 deletions
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") |