diff options
Diffstat (limited to 'HoTT.thy')
-rw-r--r-- | HoTT.thy | 7 |
1 files changed, 5 insertions, 2 deletions
@@ -6,7 +6,6 @@ Homotopy type theory theory HoTT imports - (* Basic theories *) HoTT_Base HoTT_Methods @@ -22,18 +21,22 @@ 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 + lemmas intros = 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 |