diff --git a/_chapters/06_functors.md b/_chapters/06_functors.md index d84167f..fa44c1e 100644 --- a/_chapters/06_functors.md +++ b/_chapters/06_functors.md @@ -37,14 +37,14 @@ We also defined a lot of *categories based on different things*, like the ones b Finite categories --- -And most importantly, we saw some categories that are *completely made up*, such as my soccer hierarchy. Those are formally called *finite categories* and, although they are not useful by themselves, the idea of finite categories is important - we can draw any combination of points and arrows and call it a category, in the same way that we can construct a set out of every combination of objects. +And most importantly, we saw some categories that are *completely made up*, such as my soccer player hierarchy. Those are formally called *finite categories* and, although they are not useful by themselves, the idea of finite categories is important - we can draw any combination of points and arrows and call it a category, in the same way that we can construct a set out of every combination of objects. ![Finite categories](finite_categories.svg) Examining some finite categories --- -For future reference, let's see some examples of finite categories. +For future reference, let's see some important finite categories. The simplest category is $0$ (enjoy the minimalism of this diagram.) @@ -86,22 +86,23 @@ Then, in chapter 4, we encountered *order isomorphisms* and we saw that they are Categorical isomorphisms --- -Now we will extend the definition of order isomorphisms, so it applies to categories that have more than one morphism between two objects. This will make the definition a little more complex, but not a lot. +Now we will extend the definition of order isomorphisms, so it applies to categories that have more than one morphism between two objects AKA categories different from orders. This will make the definition a little more complex, but not a lot. The definition of categorical isomorphism is the following: given two categories, an isomorphism between them is an invertible function between the underlying sets of objects, *and* an invertible function between the morphisms that connect them, which maps each morphism from one category to a morphism *with the same signature*. ![Category isomorphism](category_isomorphism.svg) -If we examine it closely we will see that, although a little bit more complex, this definition is equivalent to the one we have for orders. It is just that when categories can potentially have just one morphism, we only need to to verify that the corresponding morphism actually exist in the other category (which is guaranteed by the *order-preserving* condition.) +If we examine it closely we will see that, although it *sounds* a bit more complex, this definition is actually the same definition as one we have for orders. It is just that morphism functions between categories that have just one morphism for any two objects, are trivial - we always map the single morphism of the source category to the single morphism of the target category (which, because of the *order-preserving* condition, is guaranteed to exist.) ![Order isomorphism](category_order_isomorphism_2.svg) - -And when we can have more than one morphism between two given objects we need to make sure that each morphism in one category has a corresponding morphism in the other one. +However, when we can have more than one morphism between two given objects we need to make sure that each morphism in one category has a corresponding morphism in the other one. ![Category isomorphism](category_order_isomorphism.svg) -As you see, categorical isomorphisms are not hard to define, however there is another issue with them, namely that they are very rare in practice - the only one that comes to mind to me is the Curry-Howard-Lambek isomorphism from the last chapter. And the reason they are so rare is simple - if two categories are isomorphic, they basically contain the same data and it would be more accurate to refer to them as different *representations* of the same category than as separate categories. +As you see, categorical isomorphisms are not hard to define, however there is another issue with them, namely that they are *very rare in practice* - the only one that comes to mind to me is the Curry-Howard-Lambek isomorphism from the last chapter, as in order for them to be isomorphic, the categories they are basically the same category. We devise a more apt way to tell if two categories are equivalent, that is also more common than categorical isomorphisms, but we will do it in the next chapter. + +For now we will review a relationship that is even more abundant than isomorphisms, which are *two-way connections* between categories, namely *one-way connections* between categories, i.e. *functors*.