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: logic

Topic: Domain (op)fibration

Alexander Gietelink Oldenziel (Nov 02 2020 at 15:10):

The codomain fibration of a category with pullbacks is the basis of the categorical semantics of dependent type theory. What about the domain (op)fibration of a category with pushouts... are there any relations with type theory/logic?

Fawzi Hreiki (Nov 02 2020 at 15:11):

I've actually wondered about this before. There aren't even accepted names for the left and right adjoints to the cobase change (when they exist)

Fawzi Hreiki (Nov 02 2020 at 15:18):

This will likely have something to do with subtractive logic since the subtraction operator (left adjoint to coproduct) is dual to the exponentiation operator (right adjoint to product). The problem here though is that over categories $\mathscr{C}/X$ and hom-functors into objects Hom(-, $X$) are better behaved than under categories $X/\mathscr{C}$ and hom-functors out of objects Hom($X$, -). This is because $\mathscr{C}$ embeds into PSh($\mathscr{C}$) whereas $\mathscr{C}^{op}$ embeds into CoPSh($\mathscr{C}$).

Alexander Gietelink Oldenziel (Nov 03 2020 at 07:55):

I was thinking it could have an interpretation as a 'coindexed cotypes'. Let $C$ be a category.
A map out of an object $A$ is something like a continuation or coterm, so $A/C$ is like a category of coterms of $A$. If the category has pushouts, given $f:A \to B$ we have an induced map $C/A \to C/B$ given by pushout along $f$.