Update Plan.org

This commit is contained in:
jlh 2021-07-19 19:03:32 +01:00 committed by GitHub
parent 9a57d284f8
commit 7d9d13dc48
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23

View File

@ -63,8 +63,8 @@
+ HITs, examples + HITs, examples
- the constructed interval - the constructed interval
- booleans and covers - booleans and covers
- S^n - =S^n=
- S^1 with 2 cw structures equiv - =S^1= with 2 cw structures equiv
+ Homotopy n-types + Homotopy n-types
- homotopy levels being closed under type constructions, in particular Set and ETT inside HoTT - homotopy levels being closed under type constructions, in particular Set and ETT inside HoTT
+ in particular sigma types + in particular sigma types