You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
In #1883 I mentioned that we should consider redefining Is0Bifunctor F as Is0Functor (ucurry F). This has a few advantages:
It allows us to use our "functorial-at-the-same-time" definitions.
We don't have extra terms with the fmap01 and fmap10 split.
Bifunctor coherence becomes a lemma and a way of constructing bifunctors.
It generalised much more easily to the ternary and n-ary case.
I think we would be able to make some arguments slicker by doing this, but I haven't spent anytime really checking. It may however present other problems that I haven't thought about. I'll record this issue so that we don't forget about it.
The text was updated successfully, but these errors were encountered:
In #1883 I mentioned that we should consider redefining
Is0Bifunctor F
asIs0Functor (ucurry F)
. This has a few advantages:I think we would be able to make some arguments slicker by doing this, but I haven't spent anytime really checking. It may however present other problems that I haven't thought about. I'll record this issue so that we don't forget about it.
The text was updated successfully, but these errors were encountered: