Closed phijor closed 9 months ago
I think this looks good. Any opinions @ecavallo ?
Seems fine to me.
I marked this as ready for review so that I can make a proper review. It's nice to see that uaη has a direct proof, maybe the 1lab should be updated as well
Thanks, I took care of your requests. Once you're happy with the changes I will rebase and squash my commits.
I'm really unhappy having to add transpEquiv
to Equiv.Base
though. If #1001 gets merged, one could import from CartesianKanOps
instead of having to add unrelated definitions to such a core module.
I'm really unhappy having to add
transpEquiv
toEquiv.Base
though. If #1001 gets merged, one could import fromCartesianKanOps
instead of having to add unrelated definitions to such a core module.
But isn't transpEquiv
a very basic equivalence that fits in Equiv.Base
? I'd rather have it there than in CartesianKanOps
(which was mostly added as proof of concept and at least I did not envision it being used much elsewhere in the library)
Rebased on current master
and squashed.
But isn't
transpEquiv
a very basic equivalence that fits inEquiv.Base
?
Convinced. Let's leave it in Equiv.Base
.
I'd rather have it there than in
CartesianKanOps
(which was mostly added as proof of concept and at least I did not envision it being used much elsewhere in the library)
I see. I think coe
etc. could improve readability of some proofs (the 1lab uses it in quite a few places), but that's a discussion for another time.
While trying to resolve the duplication between
uaη
anduaTransportη
mentioned in this comment, I noticed that together withuaβ
this yields a very "cubical" proof ofunivalenceIso
, avoiding induction on paths and equivalences completely. I attempted to code-golf away the use ofisoToIsEquiv
and proveisEquivPathToEquiv
directly, but wasn't able to (at least not more efficiently).In detail, the commits do the following:
transpEquiv
toCubical.Foundations.Equiv.Base
and generalizes it to arbitrary lines of types. Arguably, this should be calledisEquivCoei→1
and live in*.CartesianKanOps
, but there's a module dependency cycle involving that and*.GroupoidLaws
that I'm not sure how to break.uaη
viaGlue
types from*.Transport
to*.Univalence
, deprecatesuaTransportη
in the former.univalenceIso
. The 1lab has a similar proof, they note however thatuaη
"is hard".I'd like some feedback on these changes,
so I'm marking this as a draft for now.In particular, I'm not sure how and where to place things in the module hierarchy, how to deprecate stuff (if at all), and whether the new proof is even better at all. Additionally, the improved proof ofuaη
is by @dolio originally, and I don't want the attribution to be lost.Pinging @mortberg who encouraged the cleanup as part of #1017.