diff options
Diffstat (limited to 'HoTT.thy')
| -rw-r--r-- | HoTT.thy | 28 |
1 files changed, 12 insertions, 16 deletions
@@ -1,44 +1,40 @@ -(* -Title: HoTT.thy -Author: Joshua Chen -Date: 2018 +(******** +Isabelle/HoTT +Feb 2019 -Homotopy type theory -*) +An experimental implementation of homotopy type theory. + +********) theory HoTT imports + (* Basic theories *) HoTT_Base HoTT_Methods (* Types *) -Coprod -Empty -Equal +Eq Nat Prod Sum -Unit +More_Types (* Derived definitions and properties *) -Equality Projections Univalence begin - text \<open>Rule bundles:\<close> lemmas intros = - Nat_intro_0 Nat_intro_succ Prod_intro Sum_intro Equal_intro Coprod_intro_inl Coprod_intro_inr Unit_intro + Nat_intro_0 Nat_intro_succ Prod_intro Sum_intro Eq_intro Cprd_intro_inl Cprd_intro_inr Unit_intro lemmas elims = - Nat_elim Prod_elim Sum_elim Equal_elim Coprod_elim Unit_elim Empty_elim + Nat_elim Prod_elim Sum_elim Eq_elim Cprd_elim Unit_elim Null_elim lemmas routines = - Nat_routine Prod_routine Sum_routine Equal_routine Coprod_routine Unit_routine Empty_routine - + Nat_routine Prod_routine Sum_routine Eq_routine Cprd_routine Unit_routine Null_routine end |