Dan Christensen

Nice! It's documented at https://coq.inria.fr/refman/addendum/universe-polymorphism.html (search for `univ_constraint`).

This feature is even more useful than I expected: if you declare some constraints, then Coq won't silently add additional constraints beyond those implied by the specification. (This doesn't seem...

That sounds too fine-grained to me. While a huge file poses problems, it's also hard to find things when they are spread among many files. In particular, I think connected...

I'd say that the name of the main file should remain unchanged. But I think you should wait until Mike gives his opinion.

I also have work in progress that relies on the join construction. Incidentally, all of the above axioms follow from a more basic consequence of the join construction, which is...

This sounds great! I won't get a chance to provide feedback, but I think these things should be quite useful. Here's one example that I was thinking about recently: by...

> Well, if you're restricting to connected types, then the form of van Kampen you get is weaker, right? The general version doesn't require connectivity. I hadn't realized that your...

I think that if we can't fix this in the HoTT library right now, we should switch Syllepsis to use the Ltac1 version of the tactic. It's only 0.9s, and...

Even 11s seems long for this kind of thing. Would it help to rethink how the data for an equivalence f is defined? Since we often use `isequiv_adjointify`, that needs...

@JasonGross Thanks for analyzing this so carefully! It seems that there are two separate issues here. One having to do with changes to `eisadj` that were introduced around Apr 10-12,...