<p>Yes, your definition does give a category. This is an instance of a somewhat general construction called <em>change of base</em> from <em>enriched</em> category theory. There is an <a href="https://ncatlab.org/nlab/show/change+of+enriching+category" rel="nofollow noreferrer">nlab page on the construction</a> but if you are a programmer you might prefer to read <a href="https://bartoszmilewski.com/2017/05/13/enriched-categories/" rel="nofollow noreferrer">Bartosz's chapter on enriched categories</a> first.</p>
<p>In fact your definition uses change of base twice. Let <span class="math-container">$C$</span> be a cartesian-closed category we think of as our programming language.</p>
<ol>
<li>First, an applicative functor is a lax monoidal functor from <span class="math-container">$F : C \to C$</span>.</li>
<li>Second, we can think of <span class="math-container">$C$</span> as enriched over itself, called <span class="math-container">$s(C)$</span>.</li>
<li>Then we can do a change of base to define a <span class="math-container">$C$</span>-enriched category <span class="math-container">$F_*(s(C))$</span> whose objects are the objects of <span class="math-container">$C$</span> and whose hom objects are <code>F(a -&gt; b)</code></li>
<li>We can define a lax monoidal functor <span class="math-container">$\Gamma : C \to \text{Set}$</span> by sending each <code>a</code> to the set of morphisms from <code>1</code> to <code>a</code>.</li>
<li>Then your category is <span class="math-container">$\Gamma_*(F_*(s(C)))$</span>.</li>
</ol>

CC BY-SA 4.0
2023-04-18T22:22:15.900Z
2023-04-18T22:28:17.217Z
2023-04-18T22:28:17.217Z
Max New
<p>Your description of that category is correct.</p>
<p>We can define a lawful category of this kind. Objects are all types <code>A</code>, <code>B</code>, ... and morphisms between <code>A</code> and <code>B</code> are values of type <code>F(A -&gt; B)</code>. The identity morphism on <code>A</code> is <code>unit(identity)</code> of type <code>F(A -&gt; A)</code>. The composition operation of type <code>F(A -&gt; B) -&gt; F(B -&gt; C) -&gt; F(A -&gt; C)</code> is defined via <code>ap</code>. The identity and associativity laws hold for that composition operation, as long as the applicative functor <code>F</code> is lawful (i.e., the laws of <code>ap</code> and <code>pure</code> hold), although it takes a bit of effort to prove that.</p>

CC BY-SA 4.0
2023-04-17T17:11:52.097Z
2023-04-18T18:33:34.207Z
2023-04-18T18:33:34.207Z
winitzki
<p>Thanks, all. Sometime after asking this, I was pointed to <a href="https://dl.acm.org/doi/pdf/10.1145/3406088.3409023" rel="nofollow noreferrer">this paper</a>, which gives a Haskell encoding of the relevant &quot;Cayley&quot; category in Sec. 3.4, p. 83.</p>

CC BY-SA 4.0
2023-04-26T11:22:54.190Z
Could you develop a bit your description of the answer described in the link?
J.y B.y
CC BY-SA 4.0
2023-04-30T23:43:03.397Z
Not entirely sure which part to develop or clarify, but I had in mind that the 'C' in my original post corresponds to the 't' quantified in the instance declaration in Sec. 3.4, while my applicative 'F' corresponds to the quantified 'f'.
Julian G.
CC BY-SA 4.0
2023-04-20T14:13:39.007Z
2023-04-20T14:13:39.007Z
Julian G.
<p>I am wondering if there is a good way to complete the following analogy:</p>
<pre><code>monad : Kleisli category :: applicative functor : ??
</code></pre>
<p>That is, a given monad <em>T</em> on a category <em>C</em> gives rise to its Kleisli category <em>C_T</em>, whose objects are those of <em>C</em>, but whose morphisms between <em>A</em> and <em>B</em> are the morphisms between <em>A</em> and <em>T(B)</em> in <em>C</em> (<a href="https://en.wikipedia.org/wiki/Kleisli_category#Formal_definition" rel="nofollow noreferrer">Wikipedia entry</a>). What I'd like to know is if there is a kind of &quot;equivalent&quot; notion for applicatives.</p>
<p>At first blush, it seems that such a category would be constructed in the following way, given a category <em>C</em> and an applicative functor (<em>F : C -&gt; C</em>, <em>pure</em>, (&lt;*&gt;)). The category <em>C_F</em> is the one whose objects are taken from <em>C</em> (as above), but whose morphisms between <em>A</em> and <em>B</em> are in one-to-one correspondence with the morphisms between <em>1</em> and <em>F(B^A)</em> in <em>C</em> - that is, &quot;elements&quot; of <em>F(B^A)</em>. In addition, identities and composition are given by:</p>
<pre><code>id_(C_F)_A = pure id_C_A

f o_(C_F) g = pure (o_C) &lt;*&gt; f &lt;*&gt; g
</code></pre>
<p>where <em>id_X_A</em> is the identity on <em>A</em> in category <em>X</em>, and (o_<em>X</em>) is composition between morphisms in <em>X</em>.</p>

CC BY-SA 4.0
2024-02-07T09:26:49.170Z
Your construction is correct, and the category laws for that category are equivalent to the usual laws of applicative functors.
winitzki
<functional-programming><ct.category-theory><monad><applicative>
Kleisli-like category for applicatives?
Julian G.
# Kleisli-like category for applicatives?

(Asked by: username_0 on 2021-04-22)

I am wondering if there is a good way to complete the following analogy:
monad : Kleisli category :: applicative functor : ??

That is, a given monad T on a category C gives rise to its Kleisli category C_T, whose objects are those of C, but whose morphisms between A and B are the morphisms between A and T(B) in C (Wikipedia entry). What I'd like to know is if there is a kind of "equivalent" notion for applicatives.
At first blush, it seems that such a category would be constructed in the following way, given a category C and an applicative functor (F : C -> C, pure, (<*>)). The category C_F is the one whose objects are taken from C (as above), but whose morphisms between A and B are in one-to-one correspondence with the morphisms between 1 and F(B^A) in C - that is, "elements" of F(B^A). In addition, identities and composition are given by:
id_(C_F)_A = pure id_C_A

f o_(C_F) g = pure (o_C) <*> f <*> g

where id_X_A is the identity on A in category X, and (o_X) is composition between morphisms in X.

**Tags:** functional-programming, ct.category-theory, monad, applicative
> **Comments:**
> **username_1**: Your construction is correct, and the category laws for that category are equivalent to the usual laws of applicative functors.  

---

## 3 answers

### Answer by username_2 on 2023-04-18. Score: 3

Yes, your definition does give a category. This is an instance of a somewhat general construction called *change of base* from *enriched* category theory. There is an [nlab page on the construction](https://ncatlab.org/nlab/show/change+of+enriching+category) but if you are a programmer you might prefer to read [Bartosz's chapter on enriched categories](https://bartoszmilewski.com/2017/05/13/enriched-categories/) first.

In fact your definition uses change of base twice. Let $C$ be a cartesian-closed category we think of as our programming language.

1. First, an applicative functor is a lax monoidal functor from $F : C \to C$.
2. Second, we can think of $C$ as enriched over itself, called $s(C)$.
3. Then we can do a change of base to define a $C$-enriched category $F\_\*(s(C))$ whose objects are the objects of $C$ and whose hom objects are `F(a -> b)`
4. We can define a lax monoidal functor $\Gamma : C \to \text{Set}$ by sending each `a` to the set of morphisms from `1` to `a`.
5. Then your category is $\Gamma\_\*(F\_\*(s(C)))$.


---

### Answer by username_1 on 2023-04-17. Score: 1

Your description of that category is correct.

We can define a lawful category of this kind. Objects are all types `A`, `B`, ... and morphisms between `A` and `B` are values of type `F(A -> B)`. The identity morphism on `A` is `unit(identity)` of type `F(A -> A)`. The composition operation of type `F(A -> B) -> F(B -> C) -> F(A -> C)` is defined via `ap`. The identity and associativity laws hold for that composition operation, as long as the applicative functor `F` is lawful (i.e., the laws of `ap` and `pure` hold), although it takes a bit of effort to prove that.


---

### Answer by username_0 on 2023-04-20. Score: 0

Thanks, all. Sometime after asking this, I was pointed to [this paper](https://dl.acm.org/doi/pdf/10.1145/3406088.3409023), which gives a Haskell encoding of the relevant "Cayley" category in Sec. 3.4, p. 83.

> **Comments:**
> **username_3**: Could you develop a bit your description of the answer described in the link?  
> **username_0**: Not entirely sure which part to develop or clarify, but I had in mind that the 'C' in my original post corresponds to the 't' quantified in the instance declaration in Sec. 3.4, while my applicative 'F' corresponds to the quantified 'f'.  

---

