From e1be5f97bb2a42b3179bc24b118d69af137f8e5d Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sat, 18 Aug 2018 21:28:21 +0200
Subject: Regrouping type rules

---
 HoTT.thy | 21 ++++++++++++++++-----
 1 file changed, 16 insertions(+), 5 deletions(-)

(limited to 'HoTT.thy')

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
-- 
cgit v1.2.3