diff options
author | Josh Chen | 2018-09-18 11:38:54 +0200 |
---|---|---|
committer | Josh Chen | 2018-09-18 11:38:54 +0200 |
commit | 6857e783fa5cb91f058be322a18fb9ea583f2aad (patch) | |
tree | c963fc0cb56157c251ad326dd28e2671ef52a2f9 /Equal.thy | |
parent | dcf87145a1059659099bbecde55973de0d36d43f (diff) |
Overhaul of the theory presentations. New methods in HoTT_Methods.thy for handling universes. Commit for release 0.1.0!
Diffstat (limited to '')
-rw-r--r-- | Equal.thy | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -44,6 +44,7 @@ axiomatization where \<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_form [form] lemmas Equal_routine [intro] = Equal_form Equal_intro Equal_elim lemmas Equal_comp [comp] |