aboutsummaryrefslogtreecommitdiff
path: root/ex/HoTT book/Ch1.thy
diff options
context:
space:
mode:
authorJosh Chen2018-08-16 16:28:50 +0200
committerJosh Chen2018-08-16 16:28:50 +0200
commitd8699451025a3bd5e8955e07fa879ed248418949 (patch)
tree46d09c26febb5617425565b0ac131b984f3b9c08 /ex/HoTT book/Ch1.thy
parent3794a2bc395264265d17243b5b707b9ed993d939 (diff)
Some comments and reorganization
Diffstat (limited to '')
-rw-r--r--ex/HoTT book/Ch1.thy (renamed from ex/HoTT Book/Ch1.thy)7
1 files changed, 7 insertions, 0 deletions
diff --git a/ex/HoTT Book/Ch1.thy b/ex/HoTT book/Ch1.thy
index 84a5cf4..65de875 100644
--- a/ex/HoTT Book/Ch1.thy
+++ b/ex/HoTT book/Ch1.thy
@@ -1,3 +1,10 @@
+(* Title: HoTT/ex/HoTT book/Ch1.thy
+ Author: Josh Chen
+ Date: Aug 2018
+
+A formalization of some content of Chapter 1 of the Homotopy Type Theory book.
+*)
+
theory Ch1
imports "../../HoTT"
begin