Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthormaxsnew
   • CommentTimeNov 28th 2017
   • (edited Nov 28th 2017)
   • PermaLink
   Author: maxsnew
   Format: MarkdownItexI've just seen an interesting abstract construction in [this paper by Mellies and Tabareau](https://hal.archives-ouvertes.fr/hal-00339156/en/) 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$?

   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$?

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeNov 29th 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexSurely the orthogonal factorization system has to be related to the adjunctions somehow?

   Surely the orthogonal factorization system has to be related to the adjunctions somehow?

3. • CommentRowNumber3.
   • CommentAuthormaxsnew
   • CommentTimeNov 29th 2017
   • PermaLink
   Author: maxsnew
   Format: MarkdownItexWhoops, 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]].

   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.

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeNov 29th 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI 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?

   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?

5. • CommentRowNumber5.
   • CommentAuthormaxsnew
   • CommentTimeNov 29th 2017
   • PermaLink
   Author: maxsnew
   Format: MarkdownItexThe 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](http://tikzcd.yichuanshen.de/#eyJub2RlcyI6W3sicG9zaXRpb24iOlswLDBdLCJ2YWx1ZSI6IkxfMVJfMWIifSx7InBvc2l0aW9uIjpbMCwxXSwidmFsdWUiOiJMXzFSXzFiJyJ9LHsicG9zaXRpb24iOlswLDJdLCJ2YWx1ZSI6ImInIn0seyJwb3NpdGlvbiI6WzIsMF0sInZhbHVlIjoiYiJ9LHsicG9zaXRpb24iOlsyLDFdLCJ2YWx1ZSI6IlJfMkxfMmIifSx7InBvc2l0aW9uIjpbMiwyXSwidmFsdWUiOiJSXzJMXzJiJyJ9XSwiZWRnZXMiOlt7ImZyb20iOjAsInRvIjozLCJ2YWx1ZSI6IlxcZXBzaWxvbl9iIn0seyJmcm9tIjoyLCJ0byI6NSwibGFiZWxQb3NpdGlvbiI6InJpZ2h0IiwidmFsdWUiOiJcXGV0YV97Yid9In0seyJmcm9tIjowLCJ0byI6MSwidmFsdWUiOiJMXzFSXzFoIn0seyJmcm9tIjo0LCJ0byI6NSwibGFiZWxQb3NpdGlvbiI6ImxlZnQiLCJ2YWx1ZSI6IlJfMkxfMmgifSx7ImZyb20iOjMsInRvIjo0LCJ2YWx1ZSI6IlxcZXRhX2IifSx7ImZyb20iOjEsInRvIjoyLCJ2YWx1ZSI6IlxcZXBzaWxvbl97Yid9In0seyJmcm9tIjozLCJ0byI6MiwidmFsdWUiOiJoIn1dfQ==). Not sure about fullness though.

   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.

6. • CommentRowNumber6.
   • CommentAuthorMike Shulman
   • CommentTimeNov 29th 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI thought it should be full by the universal property of the units and counits of the adjunctions.

   I thought it should be full by the universal property of the units and counits of the adjunctions.

7. • CommentRowNumber7.
   • CommentAuthormaxsnew
   • CommentTimeNov 29th 2017
   • PermaLink
   Author: maxsnew
   Format: MarkdownItexOh 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.

   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.