Motivation: Consider a category $\mathbf{C}$ with an object which we wish to consider as a kind of interval object $I$ (see the nlab for some possible definitions we may want to consider). Now, we have two global points $0,1 : * \to I$ of $I$, and one very natural property one might want to have on such an ``interval object'' (possibly an equivalent characterization of some of the nlab definitions?) is that all maps $f : I \to A$ should map $1$ and $0$ to the same point of $A$ (or perhaps, in a groupoid-enriched setting, equivalent points of $A$).
Question: Given a setup like the above, and some category $\mathbf{C}$ without an interval object (i.e. an object $I$ satisfying the intuitive property I gave above for interval objects), is there a natural way to adjoin one to the category in a concrete way?
Now of course, the standard categorical approach here would be something like defining a pointed "category of X categories with interval object I", and trying to construct (or at least prove the existence of) a free functor which is left adjoint to the natural forgetful functor to the "category of X's". However, what I would like to understand here is how to construct such a free functor in the most concrete way possible. More specifically, I want to try some variation on the following idea, and I wanted to know if anyone has studied similar constructions in the literature.
Idea: Given a category $\mathbf{C}$ and a subset $A$ of the set of morphisms of $\mathbf{C}$, define $\mathbf{C}\backslash A$ to be the smallest sub-category of $\mathbf{C}$ not containing any of the morphisms in $A$. Then, from this construction, the idea is that we can construct our "category with interval object" by:
- Freely adjoining an object $I$ to $\mathbb{C}$ with two points $0,1 : * \to I$ such that $I$ satisfies the universal property of $2 = 1 + 1$ (call this category $\mathbf{C}[I]$).
- Taking $\mathbf{C}[I] \backslash X$, where $X$ is the set of all morphisms in $\mathbf{C}$ not satisfying the property that $0$ and $1$ get sent to equal (or "equivalent", in whatever sense of equivalent we decide to use) points.
Some of the specific questions I had regarding this construction are:
- Has anyone considered constructions like this in the literature?
- Does this difference operator give an interesting co-heyting structure to categories?