Commit 2021-12-31 22:23 559951cd
View on Github →feat(data/quot): Add quotient pi induction (#11137) I am planning to use this later to show that the (pi) product of homotopy classes of paths is well-defined, and prove properties about that product.