Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthormaxsnew
    • CommentTimeNov 28th 2017
    • (edited Nov 28th 2017)

    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,CA,B,C and adjunctions from AA to BB and BB to CC you get a monad and a comonad on BB, and so for every object bBb \in B a morphism f b:WbbMbf_b : W b \to b \to M b. If BB further has an orthogonal factorization system, then you can recover (up to iso) bb from this map and then it is called the “fingerprint” of bb (since it uniquely identifies bb). By the adjunction this map can actually be represented as a morphism in AA or CC as well, so this means any object of BB can be represented by a morphism in AA or CC.

    In that paper the example they give is that AA is Cat, BB is MultiCat and CC is MonoidalCat with the (hopefully) obvious adjunctions. Then the fingerprint of a multicategory MM is a morphism i:Unary(M)Contexts(M)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 MM as objects and “substitutions”/sequences of arrows of MM 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 AA 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. CC is probably locally cartesian closed categories and maybe AA is Cat but then what is BB?

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeNov 29th 2017

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

    • CommentRowNumber3.
    • CommentAuthormaxsnew
    • CommentTimeNov 29th 2017

    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.

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeNov 29th 2017

    I haven’t looked at the paper, but does this embed BB full-and-faithfully in the two-sided discrete fibration associated to the profunctor from AA to CC induced by the composite adjunction?

    • CommentRowNumber5.
    • CommentAuthormaxsnew
    • CommentTimeNov 29th 2017

    The paper doesn’t talk about morphisms at all unfortunately, but it does define a functor and it is at least faithful. Given h:bbh : b \to b', it is uniquely determined by R 1hR_1h in AA and L 2hL_2h in CC by orthogonality, see this diagram.

    Not sure about fullness though.

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeNov 29th 2017

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

    • CommentRowNumber7.
    • CommentAuthormaxsnew
    • CommentTimeNov 29th 2017

    Oh yes, that’s right, the OFS means we can extract a function in BB and then that determines the original morphism because any morphism LRbbLR b \to b' has a unique factorization through LRbLRb' and the counit and vice-versa for the unit.