From 02c04555054be644868792b4b5effe968af01c02 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Wed, 17 Jul 2024 23:25:57 -0400
Subject: [PATCH] initial ch7

---
 src/HottBook/Chapter7.lagda.md | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 src/HottBook/Chapter7.lagda.md

diff --git a/src/HottBook/Chapter7.lagda.md b/src/HottBook/Chapter7.lagda.md
new file mode 100644
index 0000000..9836f60
--- /dev/null
+++ b/src/HottBook/Chapter7.lagda.md
@@ -0,0 +1,18 @@
+<details>
+  <summary>Imports</summary>
+
+```
+module HottBook.Chapter7 where
+
+open import HottBook.Chapter1
+open import HottBook.Chapter2
+open import HottBook.Chapter3
+open import HottBook.CoreUtil
+
+private
+  variable
+    l l2 : Level
+```
+
+</details>
+