Skip to main content
Fixed typo
Source Link

As Mike wrote in his comment, this statement is true with an appropriate notion of a category $\mathcal{E}^A$ and cocontinuity.

The category $\mathcal{E}^A$ from your definition is the underlying category of a locally internal category $\mathcal{E}^{\rightarrow^A}$. In more explicit terms, $\mathcal{E}^{\rightarrow}$ may be thought as of the codomain fibration over $\mathcal{E}$, $A$ as of the small fibration corresponding to the externalization of $\mathcal{E}$-internal category $A$, and $\mathcal{E}^{\rightarrow^A}$ as of the exponent $A \Rightarrow \mathcal{E}^\rightarrow$. Then your $\mathcal{E}^A$ is a mere fibre over terminal object in $\mathcal{E}^{\rightarrow^A}$.

Because for any internal category $A$$A^{op}$, fibration $\mathcal{E}^{\rightarrow^A}$$\mathcal{E}^{\rightarrow^{A}}$ is anits internal free cocompletion of $A$, we get: $$\mathit{CoCont}(\mathcal{E}^{\rightarrow^{A}}, \mathcal{E}^{\rightarrow^{B}}) \approx \hom(A^{op}, \mathcal{E}^{\rightarrow^B})$$ The above statement may be found as a special case of Theorem 3.20 in Mark Weber's "Yoneda structures from 2-toposes".

Finally: $$\hom(A^{op}, \mathcal{E}^{\rightarrow^B}) \approx \hom(1, \mathcal{E}^{\rightarrow^{A^{op} \times B}}) \approx \mathcal{E}^{A^{op}\times B}$$ where the last equivalence is an instance of fibred Yoneda lemma.

As Mike wrote in his comment, this statement is true with an appropriate notion of a category $\mathcal{E}^A$ and cocontinuity.

The category $\mathcal{E}^A$ from your definition is the underlying category of a locally internal category $\mathcal{E}^{\rightarrow^A}$. In more explicit terms, $\mathcal{E}^{\rightarrow}$ may be thought as of the codomain fibration over $\mathcal{E}$, $A$ as of the small fibration corresponding to the externalization of $\mathcal{E}$-internal category $A$, and $\mathcal{E}^{\rightarrow^A}$ as of the exponent $A \Rightarrow \mathcal{E}^\rightarrow$. Then your $\mathcal{E}^A$ is a mere fibre over terminal object in $\mathcal{E}^{\rightarrow^A}$.

Because for any internal category $A$, fibration $\mathcal{E}^{\rightarrow^A}$ is an internal free cocompletion of $A$, we get: $$\mathit{CoCont}(\mathcal{E}^{\rightarrow^{A}}, \mathcal{E}^{\rightarrow^{B}}) \approx \hom(A^{op}, \mathcal{E}^{\rightarrow^B})$$ The above statement may be found as a special case of Theorem 3.20 in Mark Weber's "Yoneda structures from 2-toposes".

Finally: $$\hom(A^{op}, \mathcal{E}^{\rightarrow^B}) \approx \hom(1, \mathcal{E}^{\rightarrow^{A^{op} \times B}}) \approx \mathcal{E}^{A^{op}\times B}$$ where the last equivalence is an instance of fibred Yoneda lemma.

As Mike wrote in his comment, this statement is true with an appropriate notion of a category $\mathcal{E}^A$ and cocontinuity.

The category $\mathcal{E}^A$ from your definition is the underlying category of a locally internal category $\mathcal{E}^{\rightarrow^A}$. In more explicit terms, $\mathcal{E}^{\rightarrow}$ may be thought as of the codomain fibration over $\mathcal{E}$, $A$ as of the small fibration corresponding to the externalization of $\mathcal{E}$-internal category $A$, and $\mathcal{E}^{\rightarrow^A}$ as of the exponent $A \Rightarrow \mathcal{E}^\rightarrow$. Then your $\mathcal{E}^A$ is a mere fibre over terminal object in $\mathcal{E}^{\rightarrow^A}$.

Because for any internal category $A^{op}$, fibration $\mathcal{E}^{\rightarrow^{A}}$ is its internal free cocompletion, we get: $$\mathit{CoCont}(\mathcal{E}^{\rightarrow^{A}}, \mathcal{E}^{\rightarrow^{B}}) \approx \hom(A^{op}, \mathcal{E}^{\rightarrow^B})$$ The above statement may be found as a special case of Theorem 3.20 in Mark Weber's "Yoneda structures from 2-toposes".

Finally: $$\hom(A^{op}, \mathcal{E}^{\rightarrow^B}) \approx \hom(1, \mathcal{E}^{\rightarrow^{A^{op} \times B}}) \approx \mathcal{E}^{A^{op}\times B}$$ where the last equivalence is an instance of fibred Yoneda lemma.

Simplified description
Source Link

As Mike wrote in his comment, this statement is true with an appropriate notion of a category $\mathcal{E}^A$ and cocontinuity.

The category $\mathcal{E}^A$ from your definition is the underlying category of a locally internal category $\mathcal{E}^{\rightarrow^A}$. In more explicit terms, $\mathcal{E}^{\rightarrow}$ may be thought as of the codomain fibration over $\mathcal{E}$, $A$ as of the small fibration corresponding to the externalization of $\mathcal{E}$-internal category $A$, and $\mathcal{E}^{\rightarrow^A}$ as of the exponent $A \Rightarrow \mathcal{E}^\rightarrow$. Then your $\mathcal{E}^A$ is a mere fibre over terminal object in $\mathcal{E}^{\rightarrow^A}$.

Because for any internal category $A$, fibration $\mathcal{E}^{\rightarrow^A}$ is an internal free cocompletion of $A$, we get: $$\mathit{CoCont}(\mathcal{E}^{\rightarrow^{A}}, \mathcal{E}^{\rightarrow^{B}}) \approx \mathit{Prof}(A^{op}, B^{op})$$$$\mathit{CoCont}(\mathcal{E}^{\rightarrow^{A}}, \mathcal{E}^{\rightarrow^{B}}) \approx \hom(A^{op}, \mathcal{E}^{\rightarrow^B})$$ The above statement may be found as a special case of Theorem 3.20 in Mark Weber's "Yoneda structures from 2-toposes".

Finally: $$\mathit{Prof}(A^{op}, B^{op}) \approx \mathit{Prof}(B, A)$$$$\hom(A^{op}, \mathcal{E}^{\rightarrow^B}) \approx \hom(1, \mathcal{E}^{\rightarrow^{A^{op} \times B}}) \approx \mathcal{E}^{A^{op}\times B}$$ is almost tautological bywhere the definition of $\mathit{Prof}$, and: $$\mathit{Prof}(B, A) \approx \mathcal{E}^{A^{op}\times B}$$ islast equivalence is an instance of fibred Yoneda lemma.

As Mike wrote in his comment, this statement is true with an appropriate notion of a category $\mathcal{E}^A$ and cocontinuity.

The category $\mathcal{E}^A$ from your definition is the underlying category of a locally internal category $\mathcal{E}^{\rightarrow^A}$. In more explicit terms, $\mathcal{E}^{\rightarrow}$ may be thought as of the codomain fibration over $\mathcal{E}$, $A$ as of the small fibration corresponding to the externalization of $\mathcal{E}$-internal category $A$, and $\mathcal{E}^{\rightarrow^A}$ as of the exponent $A \Rightarrow \mathcal{E}^\rightarrow$. Then your $\mathcal{E}^A$ is a mere fibre over terminal object in $\mathcal{E}^{\rightarrow^A}$.

Because for any internal category $A$, fibration $\mathcal{E}^{\rightarrow^A}$ is an internal free cocompletion of $A$, we get: $$\mathit{CoCont}(\mathcal{E}^{\rightarrow^{A}}, \mathcal{E}^{\rightarrow^{B}}) \approx \mathit{Prof}(A^{op}, B^{op})$$ The above statement may be found as a special case of Theorem 3.20 in Mark Weber's "Yoneda structures from 2-toposes".

Finally: $$\mathit{Prof}(A^{op}, B^{op}) \approx \mathit{Prof}(B, A)$$ is almost tautological by the definition of $\mathit{Prof}$, and: $$\mathit{Prof}(B, A) \approx \mathcal{E}^{A^{op}\times B}$$ is an instance of fibred Yoneda lemma.

As Mike wrote in his comment, this statement is true with an appropriate notion of a category $\mathcal{E}^A$ and cocontinuity.

The category $\mathcal{E}^A$ from your definition is the underlying category of a locally internal category $\mathcal{E}^{\rightarrow^A}$. In more explicit terms, $\mathcal{E}^{\rightarrow}$ may be thought as of the codomain fibration over $\mathcal{E}$, $A$ as of the small fibration corresponding to the externalization of $\mathcal{E}$-internal category $A$, and $\mathcal{E}^{\rightarrow^A}$ as of the exponent $A \Rightarrow \mathcal{E}^\rightarrow$. Then your $\mathcal{E}^A$ is a mere fibre over terminal object in $\mathcal{E}^{\rightarrow^A}$.

Because for any internal category $A$, fibration $\mathcal{E}^{\rightarrow^A}$ is an internal free cocompletion of $A$, we get: $$\mathit{CoCont}(\mathcal{E}^{\rightarrow^{A}}, \mathcal{E}^{\rightarrow^{B}}) \approx \hom(A^{op}, \mathcal{E}^{\rightarrow^B})$$ The above statement may be found as a special case of Theorem 3.20 in Mark Weber's "Yoneda structures from 2-toposes".

Finally: $$\hom(A^{op}, \mathcal{E}^{\rightarrow^B}) \approx \hom(1, \mathcal{E}^{\rightarrow^{A^{op} \times B}}) \approx \mathcal{E}^{A^{op}\times B}$$ where the last equivalence is an instance of fibred Yoneda lemma.

Source Link

As Mike wrote in his comment, this statement is true with an appropriate notion of a category $\mathcal{E}^A$ and cocontinuity.

The category $\mathcal{E}^A$ from your definition is the underlying category of a locally internal category $\mathcal{E}^{\rightarrow^A}$. In more explicit terms, $\mathcal{E}^{\rightarrow}$ may be thought as of the codomain fibration over $\mathcal{E}$, $A$ as of the small fibration corresponding to the externalization of $\mathcal{E}$-internal category $A$, and $\mathcal{E}^{\rightarrow^A}$ as of the exponent $A \Rightarrow \mathcal{E}^\rightarrow$. Then your $\mathcal{E}^A$ is a mere fibre over terminal object in $\mathcal{E}^{\rightarrow^A}$.

Because for any internal category $A$, fibration $\mathcal{E}^{\rightarrow^A}$ is an internal free cocompletion of $A$, we get: $$\mathit{CoCont}(\mathcal{E}^{\rightarrow^{A}}, \mathcal{E}^{\rightarrow^{B}}) \approx \mathit{Prof}(A^{op}, B^{op})$$ The above statement may be found as a special case of Theorem 3.20 in Mark Weber's "Yoneda structures from 2-toposes".

Finally: $$\mathit{Prof}(A^{op}, B^{op}) \approx \mathit{Prof}(B, A)$$ is almost tautological by the definition of $\mathit{Prof}$, and: $$\mathit{Prof}(B, A) \approx \mathcal{E}^{A^{op}\times B}$$ is an instance of fibred Yoneda lemma.