Reed Mullanix
Reed Mullanix
As for PERs, I think that we really want to avoid using them unless we *absolutely* have to. If Setoids are a way of taking your type theory and augmenting...
Nice catch! Was planning on porting this to the 1Lab, might be the kick in the pants I need 😁
Thanks for making the changes! That makes sense WRT `_≃ₒ_`, looks like that was wishful thinking on my end 😀 . I can hack together something that uses `Poset-path`; it...
Ah, forgot about forcing analysis :) Still think that it could be worthwhile for code re-use reasons
If you merge master into this PR, then CI should start working :)
Yes it absolutely is; haven't touched setoids for a minute obviously :) Also needs congruence lemmas everywhere.
A better name for this would be `Fam(Set)`; it is precisely the total category of the [family fibration](https://1lab.dev/Cat.Displayed.Instances.Family.html#the-family-fibration) on the category of sets. Containers/Poly would have the maps going "backwards",...
It might be worth doing `Fam` in it's generality though; this would give you `Fam(Set)`, `Fam(Setoids)`, and `Fam(Setoids^op)` all in one go.
To make (co)end calculus usable, you really need a DSL for writing "functorial forms", EG: the stuff that happens underneath the integral. If you don't have this, then things degenerate...
Yeah; things get really nasty when you have nested (co)ends, which is _exactly_ what you need for Isabelle duality.