diff options
Diffstat (limited to 'HoTT.thy')
-rw-r--r-- | HoTT.thy | 18 |
1 files changed, 11 insertions, 7 deletions
@@ -1,12 +1,13 @@ -(* Title: HoTT/HoTT.thy - Author: Josh Chen +(* +Title: HoTT.thy +Author: Joshua Chen +Date: 2018 Homotopy type theory *) theory HoTT imports - (* Basic theories *) HoTT_Base HoTT_Methods @@ -22,18 +23,21 @@ Unit (* Derived definitions and properties *) EqualProps -ProdProps Proj begin -lemmas forms = - Nat_form Prod_form Sum_form Coprod_form Equal_form Unit_form Empty_form + +text \<open>Rule bundles:\<close> + lemmas intros = - Nat_intro Prod_intro Sum_intro Equal_intro Coprod_intro Unit_intro + Nat_intro_0 Nat_intro_succ Prod_intro Sum_intro Equal_intro Coprod_intro_inl Coprod_intro_inr Unit_intro + lemmas elims = Nat_elim Prod_elim Sum_elim Equal_elim Coprod_elim Unit_elim Empty_elim + lemmas routines = Nat_routine Prod_routine Sum_routine Equal_routine Coprod_routine Unit_routine Empty_routine + end |