initial ch7
This commit is contained in:
parent
c6bc5bd952
commit
02c0455505
1 changed files with 18 additions and 0 deletions
18
src/HottBook/Chapter7.lagda.md
Normal file
18
src/HottBook/Chapter7.lagda.md
Normal file
|
@ -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>
|
||||||
|
|
Loading…
Reference in a new issue