From 76ac8ed82317f3f62f26ecc88f412c61004bcffa Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 17 Sep 2018 13:13:55 +0200
Subject: Reorganizing theories

---
 Unit.thy | 32 +++++++++++++++-----------------
 1 file changed, 15 insertions(+), 17 deletions(-)

(limited to 'Unit.thy')

diff --git a/Unit.thy b/Unit.thy
index 6760f27..61c6439 100644
--- a/Unit.thy
+++ b/Unit.thy
@@ -1,33 +1,31 @@
-(*  Title:  HoTT/Unit.thy
-    Author: Josh Chen
+(*
+Title:  Unit.thy
+Author: Joshua Chen
+Date:   2018
 
 Unit type
 *)
 
 theory Unit
-  imports HoTT_Base
-begin
+imports HoTT_Base
 
+begin
 
-section \<open>Constants and type rules\<close>
 
 axiomatization
-  Unit :: Term  ("\<one>") and
-  pt :: Term    ("\<star>") and
-  indUnit :: "[Term, Term] \<Rightarrow> Term"  ("(1ind\<^sub>\<one>)")
+  Unit    :: t  ("\<one>") and
+  pt      :: t  ("\<star>") and
+  indUnit :: "[t, t] \<Rightarrow> t"  ("(1ind\<^sub>\<one>)")
 where
-  Unit_form: "\<one>: U O"
-and
-  Unit_intro: "\<star>: \<one>"
-and
-  Unit_elim: "\<lbrakk>C: \<one> \<longrightarrow> U i; c: C \<star>; a: \<one>\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c a: C a"
-and
-  Unit_comp: "\<lbrakk>C: \<one> \<longrightarrow> U i; c: C \<star>\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c \<star> \<equiv> c"
+  Unit_form: "\<one>: U O" and
 
+  Unit_intro: "\<star>: \<one>" and
 
-text "Rule attribute declarations:"
+  Unit_elim: "\<lbrakk>a: \<one>; c: C \<star>; C: \<one> \<longrightarrow> U i\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c a: C a" and
+
+  Unit_comp: "\<lbrakk>c: C \<star>; C: \<one> \<longrightarrow> U i\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c \<star> \<equiv> c"
 
-lemmas Unit_comp [comp]
 lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_elim
+lemmas Unit_comp [comp]
 
 end
-- 
cgit v1.2.3