diff options
author | Josh Chen | 2018-08-18 21:28:21 +0200 |
---|---|---|
committer | Josh Chen | 2018-08-18 21:28:21 +0200 |
commit | e1be5f97bb2a42b3179bc24b118d69af137f8e5d (patch) | |
tree | 37fa2dacc40261bf37726e23121df0ba5b9af68e /HoTT.thy | |
parent | 03c734ea067bd28210530d862137133e2215ca80 (diff) |
Regrouping type rules
Diffstat (limited to '')
-rw-r--r-- | HoTT.thy | 21 |
1 files changed, 16 insertions, 5 deletions
@@ -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 |