Ali Caglayan

Yes, this seems to be a problem. @JasonGross is the author of this tactic.

@jdchristensen This should simplify some things in the Hurewicz branch.

I always felt like I was missing something when designing the algebra library. I feel as though there are ways to get coq to accept various casts between algebraic structures...

@jdchristensen I have spoken with the mathcomp devs also, and it has been on peoples wishlist for coq for a while now. Cyril Cohen has dubbed these "reverse coercions" and...

This will need a rebase. But I also wonder if using fmap will change anything with respect to the separate cases that were forced.

I think that the real problem here is that the order things are imported in https://github.com/HoTT/HoTT/blob/master/theories/HoTT.v are wrong. The names we actually want to use should end up last, so...

@jdchristensen We have Colimits/Quotient which is supposed to replace HIT/quotient.v. The only reason I kept the later around is because it is difficult to completely remove. It's unfortunate that it...

Actually it seems that `Cube left right front back top bottom` should really be `Cube left right back front top bottom`.

@JasonGross Do you know how to get coq to unify something like this?

@JasonGross That's an interesting solution but I am worried I am being too restrictive with the notation. It's not really a problem with the notation but with the definition of...