@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 | View the thread | More toots from mudri@mathstodon.xyz
=> View jonmsterling@mathstodon.xyz profile
text/geminiThis content has been proxied by September (3851b).