Anders Mörtberg

@ecavallo What do you want listed as your area of expertise? Most things?

> Putting this back to 'draft' - maybe it is better, if we actually use the 'Assign' field of the PRs. That way it is much easier, to get an...

Is this ready to be merged?

Merging this now. Thanks for writing it all up!

algebra for Max and synthetic homotopy/cohomology theory for Axel. how about including our Github handles with our names? On Thu, Aug 11, 2022, 11:07 Felix Cherubini ***@***.***> wrote: > ***@***.****...

I agree, let's not go down the rabbit hole of Unicode fonts... I already have trouble reading some symbols in the library in my browser (yes, I can probably sort...

@aljungstrom @ecavallo Can we golf the definition some more?

I'm confused, what does Agda.Builtin.Nat exporting Bool have to do with Unit? No matter what it seems weird that Agda.Builtin.Nat imports Agda.Builtin.Bool if it doesn't have to. Seems like an...

Ah, yes indeed the current version of the library is supposed to build on the latest release of Agda to not force us to update our Agda installations all the...

Would it be possible to set things up so that one can use `make` to typecheck only the package one is working on?