From dcf87145a1059659099bbecde55973de0d36d43f Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 18 Sep 2018 03:04:37 +0200
Subject: Theories fully reorganized. Well-formedness rules removed. New
 methods etc.

---
 Equal.thy | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'Equal.thy')

diff --git a/Equal.thy b/Equal.thy
index f9bc223..7a31e37 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -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]
-- 
cgit v1.2.3