Skip to main content
added 8 characters in body
Source Link
fosco
  • 13.6k
  • 2
  • 28
  • 77

First of all, as David Roberts pointed out in a comment above, the composition map

c :: hom a b -> hom b c -> hom a c
c f g = g . f

and the evaluation map

ev :: (a -> b) -> a -> b
ev f x = f x

share a common property, that of forming the components of a cowedge. I will now switch to category-theory notation, I'm confident you'll be able to translate back in pseudo-Haskell-ish/generic FP syntax.

Being a cowedge means that

  1. fixed objects $a,c$ of your category, the correspondence $(b,b')\mapsto \hom_{\cal A}(a,b)\times\hom_{\cal A}(b',c)$ is a functor ${\cal A}^\text{op}\times {\cal A} \to {\sf Set}$; let's call it $T$

    fixed objects $a,c$ of your category, the correspondence $(b,b')\mapsto \hom_{\cal A}(a,b)\times\hom_{\cal A}(b',c)$ is a functor ${\cal A}^\text{op}\times {\cal A} \to {\sf Set}$; let's call it $T$

  2. the family of maps $c_b : T(b,b)=\hom(a,b)\times\hom(b,c)\to \hom(a,c)$ behaves as follows, once a morphism $f : b\to b'$ is given: the square

    the family of maps $c_b : T(b,b)=\hom(a,b)\times\hom(b,c)\to \hom(a,c)$ behaves as follows, once a morphism $f : b\to b'$ is given: the square

    $$\require{AMScd}\begin{CD} T(b',b) @>T(f,b)>> T(b,b) \\ @VT(b',f)VV @VVc_bV \\ T(b',b') @>>c_{b'}> \hom(a,c) \end{CD}$$ is commutative. (I'll leave this verification to you).

$$\require{AMScd}\begin{CD} T(b',b) @>T(f,b)>> T(b,b) \\ @VT(b',f)VV @VVc_bV \\ T(b',b') @>>c_{b'}> \hom(a,c) \end{CD}$$ is commutative. (I'll leave this verification to you).

Not only this; there is a category of cowedges for $T$, i.e. families $\underline g = \{g_b : T(b,b) \to E\}$ pointing to generic sets $E$ and fitting into the same commutative squares. A morphism between a cowedge $\underline g$ and a cowedge $\underline h$ is a map between their codomains, with the property that the obvious diagram commutes (I'll leave it to you to find what is the obvious diagram). Now,

Claim. $\underline c = \{c_b : T(b,b) \to \hom(a,c)\}$ is the initial object in the category of cowedges for $T$ (a functor that, let me remind you, depends on $a,b$!).

I'll leave to you this verification.

This is the universal property of the composition maps of a category.

PS: what about the evaluation map $\text{ev} : B^A\times A \to B$? Well, in a cartesian closed category its components also form not only a cowedge (this is true in every monoidal closed category, and in fact it is true for every parametric adjunction, but nevermind); they form an initial one! In a sense, feeding a function with an element in its domain is "the simplest operation one can perform", given a function and an element (of course, this intuition deeply relies on the fact we can resort to elements; in category theory, this is often not possible). Similarly, given two arrows in a category that can be composed, composing them is the most natural thing you could do.

First of all, as David Roberts pointed out in a comment above, the composition map

c :: hom a b -> hom b c -> hom a c
c f g = g . f

and the evaluation map

ev :: (a -> b) -> a -> b
ev f x = f x

share a common property, that of forming the components of a cowedge. I will now switch to category-theory notation, I'm confident you'll be able to translate back in pseudo-Haskell-ish/generic FP syntax.

Being a cowedge means that

  1. fixed objects $a,c$ of your category, the correspondence $(b,b')\mapsto \hom_{\cal A}(a,b)\times\hom_{\cal A}(b',c)$ is a functor ${\cal A}^\text{op}\times {\cal A} \to {\sf Set}$; let's call it $T$
  2. the family of maps $c_b : T(b,b)=\hom(a,b)\times\hom(b,c)\to \hom(a,c)$ behaves as follows, once a morphism $f : b\to b'$ is given: the square

$$\require{AMScd}\begin{CD} T(b',b) @>T(f,b)>> T(b,b) \\ @VT(b',f)VV @VVc_bV \\ T(b',b') @>>c_{b'}> \hom(a,c) \end{CD}$$ is commutative. (I'll leave this verification to you).

Not only this; there is a category of cowedges for $T$, i.e. families $\underline g = \{g_b : T(b,b) \to E\}$ pointing to generic sets $E$ and fitting into the same commutative squares. A morphism between a cowedge $\underline g$ and a cowedge $\underline h$ is a map between their codomains, with the property that the obvious diagram commutes (I'll leave it to you to find what is the obvious diagram). Now,

Claim. $\underline c = \{c_b : T(b,b) \to \hom(a,c)\}$ is the initial object in the category of cowedges for $T$ (a functor that, let me remind you, depends on $a,b$!).

I'll leave to you this verification.

This is the universal property of the composition maps of a category.

PS: what about the evaluation map $\text{ev} : B^A\times A \to B$? Well, in a cartesian closed category its components also form not only a cowedge (this is true in every monoidal closed category, and in fact it is true for every parametric adjunction, but nevermind); they form an initial one! In a sense, feeding a function with an element in its domain is "the simplest operation one can perform", given a function and an element (of course, this intuition deeply relies on the fact we can resort to elements; in category theory, this is often not possible). Similarly, given two arrows in a category that can be composed, composing them is the most natural thing you could do.

First of all, as David Roberts pointed out in a comment above, the composition map

c :: hom a b -> hom b c -> hom a c
c f g = g . f

and the evaluation map

ev :: (a -> b) -> a -> b
ev f x = f x

share a common property, that of forming the components of a cowedge. I will now switch to category-theory notation, I'm confident you'll be able to translate back in pseudo-Haskell-ish/generic FP syntax.

Being a cowedge means that

  1. fixed objects $a,c$ of your category, the correspondence $(b,b')\mapsto \hom_{\cal A}(a,b)\times\hom_{\cal A}(b',c)$ is a functor ${\cal A}^\text{op}\times {\cal A} \to {\sf Set}$; let's call it $T$

  2. the family of maps $c_b : T(b,b)=\hom(a,b)\times\hom(b,c)\to \hom(a,c)$ behaves as follows, once a morphism $f : b\to b'$ is given: the square

    $$\require{AMScd}\begin{CD} T(b',b) @>T(f,b)>> T(b,b) \\ @VT(b',f)VV @VVc_bV \\ T(b',b') @>>c_{b'}> \hom(a,c) \end{CD}$$ is commutative. (I'll leave this verification to you).

Not only this; there is a category of cowedges for $T$, i.e. families $\underline g = \{g_b : T(b,b) \to E\}$ pointing to generic sets $E$ and fitting into the same commutative squares. A morphism between a cowedge $\underline g$ and a cowedge $\underline h$ is a map between their codomains, with the property that the obvious diagram commutes (I'll leave it to you to find what is the obvious diagram). Now,

Claim. $\underline c = \{c_b : T(b,b) \to \hom(a,c)\}$ is the initial object in the category of cowedges for $T$ (a functor that, let me remind you, depends on $a,b$!).

I'll leave to you this verification.

This is the universal property of the composition maps of a category.

PS: what about the evaluation map $\text{ev} : B^A\times A \to B$? Well, in a cartesian closed category its components also form not only a cowedge (this is true in every monoidal closed category, and in fact it is true for every parametric adjunction, but nevermind); they form an initial one! In a sense, feeding a function with an element in its domain is "the simplest operation one can perform", given a function and an element (of course, this intuition deeply relies on the fact we can resort to elements; in category theory, this is often not possible). Similarly, given two arrows in a category that can be composed, composing them is the most natural thing you could do.

added 686 characters in body
Source Link
fosco
  • 13.6k
  • 2
  • 28
  • 77

First of all, as David Roberts pointed out in a comment above, the composition map

c :: hom a b -> hom b c -> hom a c
c f g = g . f

and the evaluation map

ev :: (a -> b) -> a -> b
ev f x = f x

share a common property, that of forming the components of a cowedge. I will now switch to category-theory notation, I'm confident you'll be able to translate back in pseudo-Haskell-ish/generic FP syntax.

Being a cowedge means that

  1. fixed objects $a,c$ of your category, the correspondence $(b,b')\mapsto \hom_{\cal A}(a,b)\times\hom_{\cal A}(b',c)$ is a functor ${\cal A}^\text{op}\times {\cal A} \to {\sf Set}$; let's call it $T$
  2. the family of maps $c_b : T(b,b)=\hom(a,b)\times\hom(b,c)\to \hom(a,c)$ behaves as follows, once a morphism $f : b\to b'$ is given: the square

$$\require{AMScd}\begin{CD} T(b',b) @>T(f,b)>> T(b,b) \\ @VT(b',f)VV @VVc_bV \\ T(b',b') @>>c_{b'}> \hom(a,c) \end{CD}$$ is commutative. (I'll leave this verification to you).

Not only this; there is a category of cowedges for $T$, i.e. families $\underline g = \{g_b : T(b,b) \to E\}$ pointing to generic sets $E$ and fitting into the same commutative squares. A morphism between a cowedge $\underline g$ and a cowedge $\underline h$ is a map between their codomains, with the property that the obvious diagram commutes (I'll leave it to you to find what is the obvious diagram). Now,

Claim. $\underline c = \{c_b : T(b,b) \to \hom(a,c)\}$ is the initial object in the category of cowedges for $T$ (a functor that, let me remind you, depends on $a,b$!).

I'll leave to you this verification.

This is the universal property of the composition maps of a category.

PS: what about the evaluation map $\text{ev} : B^A\times A \to B$? Well, in a cartesian closed category its components also form not only a cowedge (this is true in every monoidal closed category, and in fact it is true for every parametric adjunction, but nevermind); they form an initial one! In a sense, feeding a function with an element in its domain is "the simplest operation one can perform", given a function and an element (of course, this intuition deeply relies on the fact we can resort to elements; in category theory, this is often not possible). Similarly, given two arrows in a category that can be composed, composing them is the most natural thing you could do.

First of all, as David Roberts pointed out in a comment above, the composition map

c :: hom a b -> hom b c -> hom a c
c f g = g . f

and the evaluation map

ev :: (a -> b) -> a -> b
ev f x = f x

share a common property, that of forming the components of a cowedge. I will now switch to category-theory notation, I'm confident you'll be able to translate back in pseudo-Haskell-ish/generic FP syntax.

Being a cowedge means that

  1. fixed objects $a,c$ of your category, the correspondence $(b,b')\mapsto \hom_{\cal A}(a,b)\times\hom_{\cal A}(b',c)$ is a functor ${\cal A}^\text{op}\times {\cal A} \to {\sf Set}$; let's call it $T$
  2. the family of maps $c_b : T(b,b)=\hom(a,b)\times\hom(b,c)\to \hom(a,c)$ behaves as follows, once a morphism $f : b\to b'$ is given: the square

$$\require{AMScd}\begin{CD} T(b',b) @>T(f,b)>> T(b,b) \\ @VT(b',f)VV @VVc_bV \\ T(b',b') @>>c_{b'}> \hom(a,c) \end{CD}$$ is commutative. (I'll leave this verification to you).

Not only this; there is a category of cowedges for $T$, i.e. families $\underline g = \{g_b : T(b,b) \to E\}$ pointing to generic sets $E$ and fitting into the same commutative squares. A morphism between a cowedge $\underline g$ and a cowedge $\underline h$ is a map between their codomains, with the property that the obvious diagram commutes (I'll leave it to you to find what is the obvious diagram). Now,

Claim. $\underline c = \{c_b : T(b,b) \to \hom(a,c)\}$ is the initial object in the category of cowedges for $T$ (a functor that, let me remind you, depends on $a,b$!).

I'll leave to you this verification.

This is the universal property of the composition maps of a category.

First of all, as David Roberts pointed out in a comment above, the composition map

c :: hom a b -> hom b c -> hom a c
c f g = g . f

and the evaluation map

ev :: (a -> b) -> a -> b
ev f x = f x

share a common property, that of forming the components of a cowedge. I will now switch to category-theory notation, I'm confident you'll be able to translate back in pseudo-Haskell-ish/generic FP syntax.

Being a cowedge means that

  1. fixed objects $a,c$ of your category, the correspondence $(b,b')\mapsto \hom_{\cal A}(a,b)\times\hom_{\cal A}(b',c)$ is a functor ${\cal A}^\text{op}\times {\cal A} \to {\sf Set}$; let's call it $T$
  2. the family of maps $c_b : T(b,b)=\hom(a,b)\times\hom(b,c)\to \hom(a,c)$ behaves as follows, once a morphism $f : b\to b'$ is given: the square

$$\require{AMScd}\begin{CD} T(b',b) @>T(f,b)>> T(b,b) \\ @VT(b',f)VV @VVc_bV \\ T(b',b') @>>c_{b'}> \hom(a,c) \end{CD}$$ is commutative. (I'll leave this verification to you).

Not only this; there is a category of cowedges for $T$, i.e. families $\underline g = \{g_b : T(b,b) \to E\}$ pointing to generic sets $E$ and fitting into the same commutative squares. A morphism between a cowedge $\underline g$ and a cowedge $\underline h$ is a map between their codomains, with the property that the obvious diagram commutes (I'll leave it to you to find what is the obvious diagram). Now,

Claim. $\underline c = \{c_b : T(b,b) \to \hom(a,c)\}$ is the initial object in the category of cowedges for $T$ (a functor that, let me remind you, depends on $a,b$!).

I'll leave to you this verification.

This is the universal property of the composition maps of a category.

PS: what about the evaluation map $\text{ev} : B^A\times A \to B$? Well, in a cartesian closed category its components also form not only a cowedge (this is true in every monoidal closed category, and in fact it is true for every parametric adjunction, but nevermind); they form an initial one! In a sense, feeding a function with an element in its domain is "the simplest operation one can perform", given a function and an element (of course, this intuition deeply relies on the fact we can resort to elements; in category theory, this is often not possible). Similarly, given two arrows in a category that can be composed, composing them is the most natural thing you could do.

Source Link
fosco
  • 13.6k
  • 2
  • 28
  • 77

First of all, as David Roberts pointed out in a comment above, the composition map

c :: hom a b -> hom b c -> hom a c
c f g = g . f

and the evaluation map

ev :: (a -> b) -> a -> b
ev f x = f x

share a common property, that of forming the components of a cowedge. I will now switch to category-theory notation, I'm confident you'll be able to translate back in pseudo-Haskell-ish/generic FP syntax.

Being a cowedge means that

  1. fixed objects $a,c$ of your category, the correspondence $(b,b')\mapsto \hom_{\cal A}(a,b)\times\hom_{\cal A}(b',c)$ is a functor ${\cal A}^\text{op}\times {\cal A} \to {\sf Set}$; let's call it $T$
  2. the family of maps $c_b : T(b,b)=\hom(a,b)\times\hom(b,c)\to \hom(a,c)$ behaves as follows, once a morphism $f : b\to b'$ is given: the square

$$\require{AMScd}\begin{CD} T(b',b) @>T(f,b)>> T(b,b) \\ @VT(b',f)VV @VVc_bV \\ T(b',b') @>>c_{b'}> \hom(a,c) \end{CD}$$ is commutative. (I'll leave this verification to you).

Not only this; there is a category of cowedges for $T$, i.e. families $\underline g = \{g_b : T(b,b) \to E\}$ pointing to generic sets $E$ and fitting into the same commutative squares. A morphism between a cowedge $\underline g$ and a cowedge $\underline h$ is a map between their codomains, with the property that the obvious diagram commutes (I'll leave it to you to find what is the obvious diagram). Now,

Claim. $\underline c = \{c_b : T(b,b) \to \hom(a,c)\}$ is the initial object in the category of cowedges for $T$ (a functor that, let me remind you, depends on $a,b$!).

I'll leave to you this verification.

This is the universal property of the composition maps of a category.