Lemma 2.15.4 (6)

[marcbezem]

Lemma 2.15.4 (6), the fact that the type of equivalences from a proposition P to a proposition Q is a proposition, is difficult to prove at this point. The proof that is given is wrong, Construction 2.9.9 (AKA lem:weq-iso) is not an equivalence. One would need at least that isContr(X) is a proposition. The best solution seems to be a forward reference to that fact, since the statement of 2.15.4 (6) fits really well where it is now.

[DanGrayson]

Hmm. Maybe a better proof would be to wait until we prove that being an equivalence is a proposition, and show that a subtype of a proposition is a proposition. Or better yet, change the statement to "P <=> Q is a proposition". (Who cares about equivalences between propositions, anyway?)

[marcbezem]

P ≃ Q can be useful to prove that Prop is a set, using UA. Or can that be obtained more easily? Do we have a proof that Prop is a set somewhere? I can't find it even though we use it. What also be nice to have that Set is a groupoid, etc. I we don't have them yet, these results (P ≃ Q is prop, Prop is set, Set is groupoid) could be packed together somewhere at the end of 2.15.

[bidundas]

I seem to remember that we discussed this at some point and I’d swear that the statements were included, but it probably would just add to my list of being a false witness. I agree that they must in if they aren’t there (and that we ought to cross reference back to them).

Bjorn

On Nov 29, 2022, at 10:22, Marc Bezem @.***> wrote:

P ≃ Q can be useful to prove that Prop is a set, using UA. Or can that be obtained more easily? Do we have a proof that Prop is a set somewhere? I can't find it even though we use it. What also be nice to have that Set is a groupoid, etc. I we don't have them yet, these results (P ≃ Q is prop, Prop is set, Set is groupoid) could be packed together somewhere at the end of 2.15.

— Reply to this email directly, view it on GitHub, or unsubscribe. You are receiving this because you are subscribed to this thread.

[bidundas]

That the type Set is a groupoid is claimed in Lemma 2.22.1 and that Prop is a set has the same proof and could be included in the Lemma.

That Prop is a set is used all over the place. (is a proposition …)

Btw, ”Prop” is used twice before it is defined.

Bjorn

On Nov 29, 2022, at 10:29, Bjørn Ian Dundas @.***> wrote:

I seem to remember that we discussed this at some point and I’d swear that the statements were included, but it probably would just add to my list of being a false witness. I agree that they must in if they aren’t there (and that we ought to cross reference back to them).

Bjorn

On Nov 29, 2022, at 10:22, Marc Bezem @.***> wrote:

P ≃ Q can be useful to prove that Prop is a set, using UA. Or can that be obtained more easily? Do we have a proof that Prop is a set somewhere? I can't find it even though we use it. What also be nice to have that Set is a groupoid, etc. I we don't have them yet, these results (P ≃ Q is prop, Prop is set, Set is groupoid) could be packed together somewhere at the end of 2.15.

— Reply to this email directly, view it on GitHub, or unsubscribe. You are receiving this because you are subscribed to this thread.

[marcbezem]

Good! I'll take care of Prop.

[DanGrayson]

To prove (6), consider the obvious map 𝑃 ≃ 𝑄 to (𝑃 → 𝑄) × (𝑄 → 𝑃), and call it p. Consider the fiber of p over a pair (f,g) and try to show it's contractible. The fiber consists of weq's h together with identifications of h with f in 𝑃 → 𝑄 and h^-1 with g in 𝑄 → 𝑃; the latter two types are propositions. By 2.9.9 there is an element of the fiber, namely (f,!,!). Now let (h,!,!) be some other element of the fiber. Since 𝑃 → 𝑄, isWeq(f), and isWeq(h) are propositions, we can identify f with h. Since the elements ! are elements of propositions, we can identify ! with ! and ! with !. QED

[UlrikBuchholtz]

Resolved