@zanzi Thanks for the explanation! The Maybe part in Abs does create some challenge, but as you may know, in [Fin, Set], F (Succ -) ≅ V => F (where V n = {1 ... n}), so there might be a way. I will let you know if I figure it out!
=> More informations about this toot | View the thread | More toots from zyang@mathstodon.xyz
=> View zanzi@mathstodon.xyz profile
text/geminiThis content has been proxied by September (3851b).