Ancestors

Written by James Wood on 2025-01-02 at 17:05

After a nice relaxing Christmas break, I think it's time to do some Agda hacking.

I wanted to start off with a question, but instead I'm filling in all the gaps needed to give the Poset-enriched category of sets and relations so that I can check that I'm asking the right question...

=> More informations about this toot | More toots from mudri@mathstodon.xyz

Written by James Wood on 2025-01-03 at 15:39

I think I actually want pseudomonoids on Span(Set). Or rather, on the equivalent bicategory that avoids having to use spans when I already have indexed types.

=> More informations about this toot | More toots from mudri@mathstodon.xyz

Toot

Written by James Wood on 2025-01-04 at 12:37

Urgh, I don't really want to depend on indices coming from a setoid.

=> More informations about this toot | More toots from mudri@mathstodon.xyz

Descendants

Written by Jon Sterling on 2025-01-04 at 12:42

@mudri Time to Ford...

=> More informations about this toot | More toots from jonmsterling@mathstodon.xyz

Written by James Wood on 2025-01-04 at 22:50

@jonmsterling In this case, I'm still working abstractly (doing a bunch of constructions over the category of setoids), and I hope my concrete cases can work okay with just propositional equality. The abstract stuff seems to have been going okay, except all the spam equivalence relation lemmas.

=> More informations about this toot | More toots from mudri@mathstodon.xyz