add missing coherence for TwoOneCat #1897
Conversation
theories/WildCat/TwoOneCat.v
Outdated
| @@ -10,6 +10,9 @@ Class Is21Cat (A : Type) `{Is1Cat A, !Is3Graph A} := | |||
| is1gpd_hom : forall (a b : A), Is1Gpd (a $-> b) ; | |||
| is1functor_postcomp : forall (a b c : A) (g : b $-> c), Is1Functor (cat_postcomp a g) ; | |||
| is1functor_precomp : forall (a b c : A) (f : a $-> b), Is1Functor (cat_precomp c f) ; | |||
| bifunctor_coh_comp : forall {a b c : A} {f f' : a $-> b} {g' g'' : b $-> c} | |||
There was a problem hiding this comment.
Not sure about this name. We could refactor this after #1886 and ask for composition to be a bifunctor instead.
There was a problem hiding this comment.
I'm also not sure about the direction. I've opted for $@L and $@R first but the other direction would be fine too.
There was a problem hiding this comment.
The name seems ok. I might switch the direction, since the one place it is used, it is in the other direction. It's probably most important to be consistent with Bifunctor.v, if that determines it.
theories/WildCat/TwoOneCat.v
Outdated
| @@ -10,6 +10,9 @@ Class Is21Cat (A : Type) `{Is1Cat A, !Is3Graph A} := | |||
| is1gpd_hom : forall (a b : A), Is1Gpd (a $-> b) ; | |||
| is1functor_postcomp : forall (a b c : A) (g : b $-> c), Is1Functor (cat_postcomp a g) ; | |||
| is1functor_precomp : forall (a b c : A) (f : a $-> b), Is1Functor (cat_precomp c f) ; | |||
| bifunctor_coh_comp : forall {a b c : A} {f f' : a $-> b} {g' g'' : b $-> c} | |||
There was a problem hiding this comment.
The name seems ok. I might switch the direction, since the one place it is used, it is in the other direction. It's probably most important to be consistent with Bifunctor.v, if that determines it.
|
The rest LGTM. |
Alizter
force-pushed
the
ps/rr/add_missing_coherence_for_twoonecat
branch
from
809accd to
4155e5d
Compare
|
@jdchristensen I've addressed your comments. |
|
LGTM (modulo the build failures). |
Alizter
force-pushed
the
ps/rr/add_missing_coherence_for_twoonecat
branch
from
4155e5d to
a909857
Compare
|
Oops, should be fixed now. I had changed the direction of the coherence but not updated the other files. |
We were missing the bifunctor coherence for composition. This lets us prove the exachange law in a (2,1)-category. Signed-off-by: Ali Caglayan <[email protected]> <!-- ps-id: 3254fcc0-f224-4b14-9c85-5918ad230be1 -->
…omments <!-- ps-id: 7a8dab5b-25d0-4e0d-8341-677ae85964be --> Signed-off-by: Ali Caglayan <[email protected]>
Alizter
force-pushed
the
ps/rr/add_missing_coherence_for_twoonecat
branch
from
a909857 to
07a55d8
Compare
We were missing the bifunctor coherence for composition. This lets us prove the exchange law in a (2,1)-category.