michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(hott) fix markup syntax in book.md

Browse source
This commit is contained in:
Jakob von Raumer 2016-07-18 17:27:54 +02:00 committed by Leonardo de Moura
parent 3416430cfa
commit 143bd765f3
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
hott/book.md
View file

@ -169,7 +169,7 @@ Every file is in the folder [algebra.category](algebra/category/category.md)
- 9.6 (Strict categories): [strict](algebra/category/strict.hlean) (only definition)
- 9.7 (†-categories): not formalized
- 9.8 (The structure identity principle): not formalized
- 9.9 (The Rezk completion): [constructions.rezk](algebra/category/constructions/rezk.hlean], 9.9.1 and 9.9.2 in [constructions.functor](algebra/category/constructions/functor.hlean]
- 9.9 (The Rezk completion): [constructions.rezk](algebra/category/constructions/rezk.hlean), 9.9.1 and 9.9.2 in [constructions.functor](algebra/category/constructions/functor.hlean)
Chapter 10: Set theory
----------