Functor composition
52 views
Skip to first unread message
Ernesto Acosta
May 9, 2018, 4:54:31 PM5/9/18
to HoTT Cafe
I am trying to understand the coherence condition on associativity of the composition of functors. I have asked Mike Shulman:
"In chapter 9, Category theory, page 314, Lemma 9.2.9. states that composition of functors is associative. Why do we need the coherence of this lemma? I am not sure what is the meaning of 'coherence' here and why the pentagon of equalities that follows should commute."
His answer was:
"Coherence here is meant in the same sense as coherence in a monoidal category or bicategory: associativity doesn’t hold on the nose, but coherence of the isomorphisms/paths witnessing associativity means that we don’t usually need to worry about applying them explicitly. MacLane’s coherence theorem for monoidal categories (there is a similar theorem for bicategories etc.) says that once that pentagon and triangle commute, then “all diagrams” of associativity and unit isomorphisms also commute. Thus, whenever we have two composites that differ from each other by some reassociations, we don’t need to worry about how we do the reassociation to get from one to the other; there is an essentially unique way to do it."
Now, I want to know if this is neccesary because of the way functors and their composition were defined, or if there is a way to define functors and their composition in homotopy type theory in such a way that we do not have to worry about coherence. For instance, if functors were simple functions with an additional condition we have associativity automatically without going into coherence once we check that the composition satisfies the additiional condition, or not? ( Composition of functions is associative and therefore composition of linear functions is associative because composition of linear functions is a linear function).
"In chapter 9, Category theory, page 314, Lemma 9.2.9. states that composition of functors is associative. Why do we need the coherence of this lemma? I am not sure what is the meaning of 'coherence' here and why the pentagon of equalities that follows should commute."
His answer was:
"Coherence here is meant in the same sense as coherence in a monoidal category or bicategory: associativity doesn’t hold on the nose, but coherence of the isomorphisms/paths witnessing associativity means that we don’t usually need to worry about applying them explicitly. MacLane’s coherence theorem for monoidal categories (there is a similar theorem for bicategories etc.) says that once that pentagon and triangle commute, then “all diagrams” of associativity and unit isomorphisms also commute. Thus, whenever we have two composites that differ from each other by some reassociations, we don’t need to worry about how we do the reassociation to get from one to the other; there is an essentially unique way to do it."
Now, I want to know if this is neccesary because of the way functors and their composition were defined, or if there is a way to define functors and their composition in homotopy type theory in such a way that we do not have to worry about coherence. For instance, if functors were simple functions with an additional condition we have associativity automatically without going into coherence once we check that the composition satisfies the additiional condition, or not? ( Composition of functions is associative and therefore composition of linear functions is associative because composition of linear functions is a linear function).
Reply all
Reply to author
Forward
0 new messages