Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: deprecated: id my structure

Topic: Poly + "objectwise sections"?

Bruno Gavranović (Feb 11 2023 at 17:04):

So I've got a category that is just like the category $\mathbf{Poly}$, but with more stuff (I'll call it $\mathbf{Poly}^+$). An object in $\mathbf{Poly}$ is a pair $(A, A')$, where $A : \mathbf{Set}$ and $A' : A \to \mathbf{Set}$, but an object in $\mathbf{Poly^+}$ is a triple $(A, A', s)$, where $s : (a : A) \to A'(a)$, something like a section.

A morphism $(A, A') \to (B, B')$ in $\mathbf{Poly}$ is a pair $(f, f^\sharp)$ where $f : A \to B$, and $f^\sharp: (a : A) \to B'(f(a)) \to A'(a)$.
A morphism $(A, A', s) \to (B, B', r)$ is the pair above + the condition that $\forall a : A . f^\sharp (a, r (f(a))) = s(a)$.

Is there some known categorical semantics of this?

Bruno Gavranović (Feb 11 2023 at 17:13):

If we restrict our dependent type theory to the one with only erased types, then this recovers something like a "dependent twisted arrow category".
If we then additionally require this to be non-dependent (but still erased), then this recovers a bona-fide twisted arrow category.
That is, if $A'$ and $B'$ as functions are constant (I'll call the objects they're constant on $A'$ and $B'$, overloading notation), then the sections from above turn into simple morphisms $s : A \to A'$ and $r : B \to B'$.
The forward map stays the same $f : A \to B$, but the backward map $f^\sharp : A \times B' \to A'$ is erased in $A$, meaning it's defined by $f^\sharp : B' \to A'$. This is exactly a morphism in $tw(\mathcal{C})$.