diff options
author | Josh Chen | 2019-02-22 23:45:50 +0100 |
---|---|---|
committer | Josh Chen | 2019-02-22 23:45:50 +0100 |
commit | 57d183c7955fb54b3eb6dd431f5aec338131266b (patch) | |
tree | ae6bfabbd8fcd63ee7d5140ca842599efbd58c16 /HoTT.thy | |
parent | 0036345412d5c145b63693ed672b175018fa3791 (diff) |
Cleanups and reorganization
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 |