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

the word "exists" is used before propositional truncation is defined. #129

Open DanGrayson opened 2 years ago

DanGrayson commented 2 years ago

Also attend to the few uses of "exists".

DanGrayson commented 2 years ago

Also take a look at "has" and "have".

DanGrayson commented 2 years ago

Look also at "fibrewise" and "totalization".

DanGrayson commented 2 years ago

Look also at "section".

pierrecagne commented 2 years ago

Some side-issue with the same lemma raised by Bjørn during last session:

In lemma 2.9.9 (lem:weq-iso) there is also the problem of "if and only if" which is not defined anywhere (there is one occurrence of "if and only if" before but in a comment about set theory). Because at this point univalence has not yet been introduced, there is a priori a difference between interpreting "if and only if" as "the two types are equivalent" and "there is an arrow in both direction" (even if we settle the problem of the propositional truncation for "exists"). I think we want the latter here, but the point is that a careful student could be very confused.

DanGrayson commented 2 years ago

We should use "if and only if" only with propositions on both sides, and it should be defined to mean there is a map in both directions.

pierrecagne commented 2 years ago

Seems like a good convention to me.

Just to recall in writing something that have been said orally: we should probably avoid doing the same kind of convention for "if", as it would prevent very natural phrasing as "if x is an element of type X [...]" where the "if" is used at a meta level (the subordinate clause of "if" being a whole judgment there).