@jonmsterling I was shooting for an equivalence in the case where the family is propositionally-valued only. Shouldn't it work in that case?
Hmm, I suppose there is no guarantee that the existence property won't muck about and mess with the witnesses. Good point.
=> More informations about this toot | View the thread | More toots from andrejbauer@mathstodon.xyz
=> View jonmsterling@mathstodon.xyz profile
text/geminiThis content has been proxied by September (ba2dc).