blob: e5db6736f17981215f1874a3ab6258fb6151cad2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
(********
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
|
