Mike Shulman
Mike Shulman
Because the path-constructors of a HIT are axioms that aren't visible when the type itself is defined as a `Private Inductive`, the size of their inputs doesn't affect the size...
It seems likely that a lot of the slowness of `V.v` is due to its insane number of universe parameters (e.g. `V.function` has over 2000). We should experiment with adding...
Let's try to keep the dependencies of directories as simple as possible. In particular, I'd like to remove the dependency on Freudenthal from pSusp and simply put that lemma into...
The action of a functor `X_functor` on homotopies is variously called `X_functor_homotopy`, `X_functor_htpy`, and `X_2functor`. We should be consistent.
Cleaning out my inbox, I found this suggested in an old email thread.
Consider the following code: ```coq Definition foo {X : Type} (f : X -> X) := True. Definition E := { p : forall X, X & True }. Definition...
The absence of this confused someone on Zulip. We often don't bother to mention it, but I think it's consistent to mention it when we're mentioning "the characterization of paths...