diff options
Diffstat (limited to '')
-rw-r--r-- | Equal.thy | 10 |
1 files changed, 5 insertions, 5 deletions
@@ -7,7 +7,7 @@ Equality type *) theory Equal -imports HoTT_Base HoTT_Methods +imports HoTT_Base begin @@ -36,13 +36,13 @@ axiomatization where p: x =\<^sub>A y; x: A; y: A; - \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i; - \<And>x. x: A \<Longrightarrow> f x: C x x (refl x) \<rbrakk> \<Longrightarrow> ind\<^sub>= (\<lambda>x. f x) p : C x y p" and + \<And>x. x: A \<Longrightarrow> f x: C x x (refl x); + \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i \<rbrakk> \<Longrightarrow> ind\<^sub>= (\<lambda>x. f x) p : C x y p" and Equal_comp: "\<lbrakk> a: A; - \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i; - \<And>x. x: A \<Longrightarrow> f x: C x x (refl x) \<rbrakk> \<Longrightarrow> ind\<^sub>= (\<lambda>x. f x) (refl a) \<equiv> f a" + \<And>x. x: A \<Longrightarrow> f x: C x x (refl x); + \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i \<rbrakk> \<Longrightarrow> ind\<^sub>= (\<lambda>x. f x) (refl a) \<equiv> f a" lemmas Equal_routine [intro] = Equal_form Equal_intro Equal_elim lemmas Equal_comp [comp] |