aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--HoTT_Base.thy4
-rw-r--r--Prod.thy19
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>
diff --git a/Prod.thy b/Prod.thy
index 48f0151..0bd037d 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -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"