Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I’ve just seen an interesting abstract construction in this paper by Mellies and Tabareau on page 19 and I’m curious if people have other examples.
They call it the “fingerprint”. Given 3 categories $A,B,C$ and adjunctions from $A$ to $B$ and $B$ to $C$ you get a monad and a comonad on $B$, and so for every object $b \in B$ a morphism $f_b : W b \to b \to M b$. If $B$ further has an orthogonal factorization system, then you can recover (up to iso) $b$ from this map and then it is called the “fingerprint” of $b$ (since it uniquely identifies $b$). By the adjunction this map can actually be represented as a morphism in $A$ or $C$ as well, so this means any object of $B$ can be represented by a morphism in $A$ or $C$.
In that paper the example they give is that $A$ is Cat, $B$ is MultiCat and $C$ is MonoidalCat with the (hopefully) obvious adjunctions. Then the fingerprint of a multicategory $M$ is a morphism $i : Unary(M) \to Contexts(M)$ in Cat from the category of unary morphisms to the monoidal category of “contexts” that has sequences of objects of $M$ as objects and “substitutions”/sequences of arrows of $M$ as arrows.
This seems very similar to the presentation of models of simple type theory taking as objects contexts and then having a subset of display objects to represent the actual types. In fact, I think you can make this presentation an instance of “fingerprint” if you take $A$ to be Set and compose with the discrete cat/set of objects adjunction to get an adjunction from Set to MultiCat.
The construction is obviously very general though, does anyone see any other natural examples (or perhaps a different name for fingerprint)? I would hope that a presentation of models of dependent type theories would have a similar formulation, but I’m not sure what the categories would be. $C$ is probably locally cartesian closed categories and maybe $A$ is Cat but then what is $B$?
Surely the orthogonal factorization system has to be related to the adjunctions somehow?
Whoops, you’re right, you need that the counit, unit combination is a factorization, that the counit is from E send unit is from M so that you can recover the object.
Also the factorization used in the multicategory example is the multicategory version of the (bo, ff) factorization system.
I haven’t looked at the paper, but does this embed $B$ full-and-faithfully in the two-sided discrete fibration associated to the profunctor from $A$ to $C$ induced by the composite adjunction?
The paper doesn’t talk about morphisms at all unfortunately, but it does define a functor and it is at least faithful. Given $h : b \to b'$, it is uniquely determined by $R_1h$ in $A$ and $L_2h$ in $C$ by orthogonality, see this diagram.
Not sure about fullness though.
I thought it should be full by the universal property of the units and counits of the adjunctions.
Oh yes, that’s right, the OFS means we can extract a function in $B$ and then that determines the original morphism because any morphism $LR b \to b'$ has a unique factorization through $LRb'$ and the counit and vice-versa for the unit.
1 to 7 of 7