Indexed products and coproducts #1878
Conversation
|
@jdchristensen This should set us up nicely to investigate limits eventually (in a later PR). Note that as expected, there is no coherence on the indexing type |
theories/WildCat/Bifunctor.v
Outdated
| Global Instance is0functor_bifunctor01 {A B C : Type} | ||
| `{Is01Cat A} `{IsGraph B} `{IsGraph C} | ||
| (F : A * B -> C) `{!Is0Functor F} (a : A) | ||
| : Is0Functor (fun b => F (a, b)). |
There was a problem hiding this comment.
The material here is using bifunctor in a slightly different way. Earlier, it means F : A -> B -> C with certain properties.
-
I think we should distinguish between the two types, but am not sure of the best name.
-
Maybe these results should be combined to prove that a bifunctor of the type
F : A * B -> Cgives rise to a bifunctor of the typeF : A -> B -> C, since that's missing. Then the results about functoriality in each variable follow. (Or these separate results could be kept, with followup results giving the IsBifunctor structure?) -
I'm not sure we actually need these results. I'll make another comment about this in the place where these are used.
| Class Is1Bifunctor {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C} | ||
| (F : A -> B -> C) `{!IsBifunctor F} | ||
| := { | ||
| bifunctor_is1functor_10 :: forall a : A, Is1Functor (F a); |
There was a problem hiding this comment.
I followed the convention above here, but IMO it's more consistent to remove the final underscores and switch the 10 / 01 suffixes. In my mind bifunctor_is0functor01 should mean that you can fmap in the second argument.
There was a problem hiding this comment.
Rather than using indexes maybe we could write _fst and _snd? The index is not immediately understandably IMO.
There was a problem hiding this comment.
I think either 01/10 without the underscore or _fst/_snd are both fine.
|
After finishing the review comments in #1884 and merging, I will take another look at this PR. |
Signed-off-by: Ali Caglayan <[email protected]>
WildCat/Products.v: Add to indexed products WildCat/Products.v: cleanup Fix indexed product functor Initial implementation of indexed coproducts Build indexed products and coproducts Alternative proofs of functoriality of binary prod Replace proofs of functoriality for binary product Clean up indexed products and coproducts Revert proofs of functoriality for binary products Clean up indexed products and coproducts
|
@Alizter should I squash this, or is the protocol to squash all commits before a PR and keep the review commits? |
|
@gio256 I think it is fine not to squash this one. I'm currently having another look and once I am done I will merge as is. |
|
Something interesting that I noticed was that we don't need |
That's interesting. This is a spot where the 0-groupoid structure isn't quite working in our favour. We do have an equivalence of types between |
|
I forgot to prove that Type has all coproducts. Thanks! |
|
@gio256 Thanks a lot! This turned out nicely. |
|
Thanks for the careful feedback, @Alizter @jdchristensen! |
Generalizes binary products and coproducts to indexed products and coproducts, building on work by @Alizter.
The primary changes are to
WildCat/Products.vandWildCat/Coproducts.v, i.e. I haven't touched any of the places where binary products and coproducts are currently used, but that may be ripe for another PR.