search

UniMath / SymmetryBook

This book will be an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.
Creative Commons Attribution Share Alike 4.0 International
378 stars 22 forks source link

Theorem 2.26.4 #172

Closed marcbezem closed 1 year ago

marcbezem commented 1 year ago

Theorem 2.26.4 is formulated as an exercise, but the last sentence just before it reads "so we give a full proof", suggesting otherwise. I think a theorem is better here, as it would be a hard exercise, even though it is prepared by Exc. 2.17.12 (which is doable). BTW to avoid the formulation "each such factorization is equivalent" Thm. 2.26.4, I would propose defining the type of factorizations and prove that it is contractible. Perhaps also rephrase Exc. 2.17.12 in this sense.

UlrikBuchholtz commented 1 year ago

I agree that we should define (in symbols) the type of factorizations the first time this is needed, in 2.17.12. Then we can be less precise later on.

marcbezem commented 1 year ago

Done, see 25d93b709d35f258d13a610 However, working on this I changed my view on Thm. 2.26.4: it is premature, 0-connected and 0-trucated are not defined, and everything is done better in 3.9, Higher images. Hence my proposal is to delete Thm. 2.26.4.

marcbezem commented 1 year ago

I swapped 2.26 and 2.27, since the old 2.26 mentioned general $n$-truncation (in old foornote 74), and this was defined in old 2.27. Also, old 2.26, at least in my view, works better as a last section of the chapter, a little informal with "stuff", "forgets at most" etc. Like the last lecture before a long holiday. So, after 2f8c8932378bd389 we should still discuss what we want with Theorem (now) 2.27.4.

UlrikBuchholtz commented 1 year ago

Done!