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 @@ +
+ Imports + +``` +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 +``` + +
+