cubical-demo Multiple ≃'s

Multiple ≃'s

Open fredefox opened this issue 7 years ago • 2 comments

Cubical._≃_ is defined via Σ. Cubical.Univalence._≃_ is congruent but defined via a record.

What's the motivation? Would you mind it if I let Cubical.Univalence import and use the one defined in PathPrelude?

Mar 08 '18 11:03 fredefox

I can see that maybe you crucially need no-eta-equality.

What if I in stead define \simeq in PathPrelude? Would that be agreeable?

Mar 08 '18 11:03 fredefox

Sigh. It seems that eta-equality is needed in PathPrelude...

Mar 08 '18 12:03 fredefox