diff options
author | Josh Chen | 2020-04-02 17:57:48 +0200 |
---|---|---|
committer | Josh Chen | 2020-04-02 17:57:48 +0200 |
commit | c2dfffffb7586662c67e44a2d255a1a97ab0398b (patch) | |
tree | ed949f5ab7dc64541c838694b502555a275b0995 /HoTT.thy | |
parent | b01b8ee0f3472cb728f09463d0620ac8b8066bcb (diff) |
Brand-spanking new version using Spartan infrastructure
Diffstat (limited to 'HoTT.thy')
-rw-r--r-- | HoTT.thy | 40 |
1 files changed, 0 insertions, 40 deletions
diff --git a/HoTT.thy b/HoTT.thy deleted file mode 100644 index e5db673..0000000 --- a/HoTT.thy +++ /dev/null @@ -1,40 +0,0 @@ -(******** -Isabelle/HoTT -Feb 2019 - -An experimental implementation of homotopy type theory. - -********) - -theory HoTT -imports - -(* Basic theories *) -HoTT_Base -HoTT_Methods - -(* Types *) -Eq -Nat -Prod -Sum -More_Types - -(* Derived definitions and properties *) -Projections -Univalence - -begin - -text \<open>Rule bundles:\<close> - -lemmas intros = - 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 Eq_elim Cprd_elim Unit_elim Null_elim - -lemmas routines = - Nat_routine Prod_routine Sum_routine Eq_routine Cprd_routine Unit_routine Null_routine - -end |