Emily Riehl
Emily Riehl
Thanks. BTW this is how I discovered my problem with apt_pkg and the missing inputs to dpkg. I tried to update to Ubuntu 22.04 but couldn't since I have various...
> Note: Moving files to `SimplicialSet.*` should be done in a separate PR doing only that. See PR #17620.
> I think the new file can be wrapped in a `namespace SSet`. @jcommelin to clarify, you were suggesting moving `HomotopyCat.lean` out of the `CategoryTheory` namespace and into the `SSet`...
@joelriou this makes the cuts that you requested and is now ready for review.
Two comments for @joelriou: 1. For whatever reason I have to write `SSet.Truncated.HomotopyCategory.quotientFunctor V` even in the `SSet.Truncated` namespace. 2. I'm not sure how much of this file should be...
I may have figured out the issue: most of this file is actually in the `CategoryTheory.SSet.Truncated` namespace. Which further suggests I've made the namespaces all wrong.
@joelriou the current version adds the constructions of isomorphisms in `Quiv` and `ReflQuiv` as requested. Then the `HomotopyCat` file contains two versions of `OneTruncation₂.ofNerve₂.natIso` for comparison. The first version, starting...
Thanks @joelriou. I really appreciate all your efforts and am sorry this has proven so painful to review! (I'm working now on the final PR in this series to work...
Sorry about that. I don't understand what happened. But it should be fixed now.
This is now ready for review (as far as I can tell).