Regrouping type rules

1 files changed, 16 insertions, 5 deletions

diff --git a/HoTT.thy b/HoTT.thy
index 724eebc..789eed2 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -1,7 +1,7 @@
 (*  Title:  HoTT/HoTT.thy
     Author: Josh Chen
 
-Load all the component modules for the HoTT logic.
+Homotopy type theory
 *)
 
 theory HoTT
@@ -12,15 +12,26 @@ HoTT_Base
 HoTT_Methods
 
 (* Types *)
-Prod
-Sum
-Equal
 Coprod
+Equal
 Nat
+Prod
+Sum
 
-(* Additional properties *)
+(* Derived definitions and properties *)
 EqualProps
+ProdProps
 Proj
 
 begin
+
+lemmas form_rules =
+  Nat_form Prod_form Sum_form Coprod_form Equal_form Unit_form Empty_form
+lemmas intro_rules =
+  Nat_intro Prod_intro Sum_intro Equal_intro Coprod_intro Unit_intro
+lemmas elim_rules =
+  Nat_elim Prod_elim Sum_elim Equal_elim Coprod_elim Unit_elim Empty_elim
+lemmas routine_rules =
+  Nat_routine Prod_routine Sum_routine Equal_routine Coprod_routine Unit_routine Empty_routine
+
 end