Dagur Asgeirsson

icon location Reykjavik, Iceland

Results 27 comments of Dagur Asgeirsson

feat(CategoryTheory): transport Kan extensions via equivalences

Thanks for the ping. I'll take a look but I don't have time until tomorrow evening

feat(CategoryTheory): the localized category is monoidal

I just opened #18165 which, if merged, should avoid random merge conflicts appearing here.

feat(CategoryTheory/Sites): the topology is generated by 1-hypercovers

Yes, I think I already reviewed and approved?

refactor(Topology/Category): refactor CompHaus.Basic

bors merge

refactor(Topology/Category): refactor CompHaus.Basic

bors merge

feat(Condensed): characterisation of discrete (light) condensed sets and modules

> ### PR summary [92528ad914](https://github.com/leanprover-community/mathlib4/pull/14027/commits/92528ad9140a8a8a7888d32231b57dcc99097709) > Import changes exceeding 2% > > % File > +4.37% `Mathlib.Algebra.Category.ModuleCat.FilteredColimits` > #### Import changes for modified files > #### Declarations diff I think...

feat(Condensed): characterisation of discrete (light) condensed sets and modules

Thanks for all the reviews 🎉 bors merge

feat(CategoryTheory/Monoidal): Hopf monoids

Thanks! maintainer merge

feat(CategoryTheory/Monoidal): Hopf monoids

Let's try again: maintainer merge

feat(LightCondensed): the functor from `TopCat`

This is independent of the refactor of `LightProfinite`. See #13504