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
371 stars 22 forks source link

2.24.2-4 #164

Closed marcbezem closed 10 months ago

marcbezem commented 1 year ago

I think we have to reformulate Exc. 2.24.2, parts (2) and (3) to "Give equivalences ..." The formulation of Lemma 2.24.4 (not yet updated, = is still meaning truncated -=->), part (2), should become something like "the function which is the identity on the first components is an equivalence ...". The proof has to be rewritten drastically (but is not difficult).

DanGrayson commented 1 year ago

Also: the equal sign in X = n is inappropriate. The expression should be replaced by the propositional truncation of X --=-> n.

marcbezem commented 1 year ago

See e3dd1c4bd7