michael/type-theory
2
0
Fork 0
Code Issues 21 Pull requests Projects 1 Releases 1 Packages Wiki Activity Actions

auto gitdoc commit

Browse source
This commit is contained in:
Michael Zhang 2024-04-22 01:45:52 +00:00
parent abde273e80
commit 2e416a404f
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/HottBook/Chapter2Exercises.lagda.md
View file

@ -9,8 +9,8 @@ open import HottBook.Util
## Exercise 2.4
Define, by induction on n, a general notion of n-dimensional path in a type A,
simultaneously with the type of boundaries for such paths.
_Define, by induction on n, a general notion of n-dimensional path in a type
$A$, simultaneously with the type of boundaries for such paths._
(tracked in [#6][6])
@ -29,7 +29,7 @@ Prove that the functions [2.3.6] and [2.3.7] are inverse equivalences.
### Exercise 2.13
Show that (2 ≃ 2) ≃ 2.
_Show that $(2 \simeq 2) \simeq 2$._
```
exercise2∙13 : (𝟚 ≃ 𝟚) ≃ 𝟚