aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--HoTT_Base.thy9
-rw-r--r--Prod.thy5
2 files changed, 9 insertions, 5 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 88cf986..e74ef31 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -68,16 +68,19 @@ text \<open>We use the notation @{prop "B: A \<leadsto> U i"} to abbreviate type
section \<open>Named theorems\<close>
-named_theorems comp
named_theorems form
+named_theorems comp
+named_theorems cong
text \<open>
The named theorems above will be used by proof methods defined in @{file HoTT_Methods.thy}.
-@{attribute comp} declares computation rules, which are used by the \<open>compute\<close> method, and may also be passed to invocations of the method \<open>subst\<close> to perform equational rewriting.
-
@{attribute form} declares type formation rules.
These are mainly used by the \<open>cumulativity\<close> method, which lifts types into higher universes.
+
+@{attribute comp} declares computation rules, which are used by the \<open>compute\<close> method, and may also be passed to invocations of the method \<open>subst\<close> to perform equational rewriting.
+
+@{attribute cong} declares congruence rules, the definitional equality rules of the type theory.
\<close>
(* Todo: Set up the Simplifier! *)
diff --git a/Prod.thy b/Prod.thy
index a28c52a..0de7d89 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -66,6 +66,7 @@ Note that this is a separate rule from function extensionality.
lemmas Prod_form [form]
lemmas Prod_routine [intro] = Prod_form Prod_intro Prod_elim
lemmas Prod_comp [comp] = Prod_cmp Prod_uniq
+lemmas Prod_cong [cong] = Prod_form_eq Prod_intro_eq
section \<open>Function composition\<close>
@@ -98,12 +99,12 @@ end
lemma compose_assoc:
assumes "A: U i" "f: A \<rightarrow> B" "g: B \<rightarrow> C" "h: TT x: C. D x"
shows "compose A (compose B h g) f \<equiv> compose A h (compose A g f)"
-by (derive lems: assms Prod_intro_eq)
+by (derive lems: assms cong)
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 "(,\\x: B. c x) o (,\\x: A. b x) \<equiv> ,\\x: A. c (b x)"
-by (derive lems: assms Prod_intro_eq)
+by (derive lems: assms cong)
abbreviation id :: "t \<Rightarrow> t" where "id A \<equiv> ,\\x: A. x"