diff options
| -rw-r--r-- | HoTT_Base.thy | 4 | ||||
| -rw-r--r-- | Prod.thy | 19 |
2 files changed, 16 insertions, 7 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 34474d1..ee36af4 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -66,8 +66,8 @@ where "f: A \<leadsto> B \<equiv> (\<And>x. x: A \<Longrightarrow> f x: B)" text \<open>We use the notation @{prop "B: A \<leadsto> U i"} to abbreviate type families.\<close> -abbreviation (input) K_combinator :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" ("^_" [1000]) -where "^A \<equiv> \<lambda>_. A" +abbreviation (input) K_combinator :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" ("&_" [0] 3) +where "&A \<equiv> \<lambda>_. A" section \<open>Named theorems\<close> @@ -96,17 +96,26 @@ in end \<close> -lemma compose_assoc: - assumes "A: U i" and "f: A \<rightarrow> B" and "g: B \<rightarrow> C" and "h: \<Prod>x: C. D x" - shows "(h o[B] g) o[A] f \<equiv> h o[A] g o[A] f" -unfolding compose_def by (derive lems: assms cong) +lemma compose_type: + assumes + "A: U i" and "B: U i" and "C: B \<leadsto> U i" and + "f: A \<rightarrow> B" and "g: \<Prod>x: B. C x" + shows "g o[A] f: \<Prod>x: A. C (f`x)" +unfolding compose_def by (derive lems: assms) lemma compose_comp: assumes "A: U i" and "\<And>x. x: A \<Longrightarrow> b x: B" and "\<And>x. x: B \<Longrightarrow> c x: C x" shows "(\<lambda>x: B. c x) o[A] (\<lambda>x: A. b x) \<equiv> \<lambda>x: A. c (b x)" unfolding compose_def by (derive lems: assms cong) -declare compose_comp [comp] +declare + compose_type [intro] + compose_comp [comp] + +lemma compose_assoc: + assumes "A: U i" and "f: A \<rightarrow> B" and "g: B \<rightarrow> C" and "h: \<Prod>x: C. D x" + shows "(h o[B] g) o[A] f \<equiv> h o[A] g o[A] f" +unfolding compose_def by (derive lems: assms cong) abbreviation id :: "t \<Rightarrow> t" where "id A \<equiv> \<lambda>x: A. x" |