HoTT.thy


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

(*  Title:  HoTT/HoTT.thy
    Author: Josh Chen

Load all the component modules for the HoTT logic.
*)

theory HoTT

imports

(* Basic theories *)
HoTT_Base
HoTT_Methods

(* Types *)
Equal
Prod
Sum

(* Additional properties *)
EqualProps
Proj

begin
end