diff options
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 |