diff options
author | Josh Chen | 2018-09-18 03:04:37 +0200 |
---|---|---|
committer | Josh Chen | 2018-09-18 03:04:37 +0200 |
commit | dcf87145a1059659099bbecde55973de0d36d43f (patch) | |
tree | 03707f3dc962e6b762890cff92cb106834b879bc /Equal.thy | |
parent | 49c008ef405ab8d8229ae1d5b0737339ee46e576 (diff) |
Theories fully reorganized. Well-formedness rules removed. New methods etc.
Diffstat (limited to 'Equal.thy')
-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] |