blob: 6c6ad21c4cee66dbf95fabfe37ca19a35e7a1ecf (
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
41
42
43
44
|
(*
Title: HoTT.thy
Author: Joshua Chen
Date: 2018
Homotopy type theory
*)
theory HoTT
imports
(* Basic theories *)
HoTT_Base
HoTT_Methods
(* Types *)
Coprod
Empty
Equal
Nat
Prod
Sum
Unit
(* 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
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
|
