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

[DanGrayson]

[DanGrayson]

Also attend to the few uses of "exists".

[DanGrayson]

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

[DanGrayson]

Look also at "fibrewise" and "totalization".

[DanGrayson]

Look also at "section".

[pierrecagne]

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]

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]

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).