Ali Caglayan

@JasonGross if you pop over to TorusEquivCircles.v and stick in `refine ((sq_ap2_compose c2t' t2c loop loop) @lr _).` right after `1,2,3,4: exact (eisretr _ _)^.` in `c2t2c` it doesn't work....

@JasonGross I was trying to extract the code into something that runs in regular coq. What's weird is that it now runs. Observe that the following works in regular coq,...

@JasonGross Thanks for working that out!

This doesn't seem to be a bug in coq after returning to it. The Symmetric class forces both universe instances of ` Equiv@{u v} : Type@{u} -> Type@{v} -> Type@{max(u,v)}...

Here is a more minimized version of the issue: ```coq Set Universe Polymorphism. (** Relations *) Definition Relation (A : Type) := A -> A -> Type. Class Symmetric {A}...

I kind of like Mike's idea of making symmetry clever. I have some ideas how we could make this happen, I'll try experimenting. It has annoyed me for some time...

We should try to clean up some of these instances as they could be causing speed issues in various places.

@andrejbauer AFAIK both currently work.

This is essentially about characterizing dependent paths over sigmas right? I tried this a while back and got very stuck. I would have heuristically guessed something like "DPaths between sigmas"...

It seems that my renaming of Nat has been too eager and has changed some comments. Let me fix those.