Add univalence as an explicit definition about cubical HOT 10 CLOSED

I came up with a slick proof of the standard formulation now:

https://github.com/agda/cubical/blob/master/Cubical/Basics/Univalence.agda#L56

So closing this issue.

from cubical.

Sure @martinescardo ! I'll reopen the issue and do it.

How does this proof compare to other proofs of univalence that you know? I think it is quite slick and it doesn't use uabeta which is something I see as a big plus! (the direct proof of uabeta in cubicaltt relies on how the Kan operations compute which is not very good as it will break if we change the operational semantics...).

from cubical.

I finished the proof of the more standard formulation of univalence for Id types now: https://github.com/agda/cubical/blob/master/Cubical/Basics/UnivalenceId.agda

from cubical.

We also have ua in the same file. But I agree it would be nice to have the proof that ua is an equivalence.

from cubical.

Sure, I wouldn't be surprised if given the above kit and ua, the definition of univalence is just a one-liner. But it's not obvious to me what that one line would be.

from cubical.

Yes, I totally agree that we should have more standard formulations of univalence (in the Cubical/Basics folder). Felix Wellen is actually already working on this, so we should have it in a not too distant future.

In the meantime I'll add some comments explaining why this is equivalent to the standard formulation of univalence with a pointer to the right section in the HoTT book.

from cubical.

I added some clarification to the core library now: 063cf7d

from cubical.

Can you also add this for the identity type?

from cubical.

Nice. The proof I have uses Yoneda, but I think it may be "the same" when unfolded. Yoneda itself doesn't rely on *beta, and the *beta part is automatic. http://www.cs.bham.ac.uk/~mhe/agda-new/UF-Yoneda.html#15981

from cubical.

Thanks!

from cubical.