Prove if A and B are sets, then A = B is also a set

[u594...@gmail.com]

I remember we have used this result in multiple places in the book, but no proof is found. I am struggling on proving it. It confuses me for some time. Could someone here please help with this?

We may try proving A \simeq B is a set, but it still leads me nowhere.

[Cory Knapp]

A sketch is as follows:

A=B is equivalent to A~B by univalence, and this is a subtype of A->B, since isEquiv is a proposition. If B is a set, then for any type A, the type A->B is also a set.

On Fri, Mar 15, 2019, 12:08 <u594...@gmail.com> wrote:

I remember we have used this result in multiple places in the book, but no proof is found. I am struggling on proving it. It confuses me for some time. Could someone here please help with this?

We may try proving A \simeq B is a set, but it still leads me nowhere.

--
You received this message because you are subscribed to the Google Groups "HoTT Cafe" group.
To unsubscribe from this group and stop receiving emails from it, send an email to hott-cafe+...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Ali Caglayan]

Can this be done without univalence?

[Cory Knapp]

You certainly need function extensionality, and maybe proposition extensionality. But with some care the same argument goes through (using instead that A=B is a subtype of A~B)---I can't see the details will enough to know if propext is needed without working out the argument more precisely.

[Michael Shulman]

I wouldn't expect there is any way to prove much of anything about
A=B for types A,B without using univalence. Why do you say that A=B
is a subtype of A~B?

[Anders Mortberg]

Just a minor remark: we only need to use that A=B is a retract of A~B
to prove this.

I believe this is equivalent to the standard formulation of
univalence, but in a system like cubical type theory it is a little
easier to construct a term for this retraction than constructing a
term for the standard formulation of univalence so I prefer using this
formulation of univalence for this proof.

--
Anders

[Yiming Xu]

Thank you a lot! I think I get it.