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.
    • CommentAuthorjim_stasheff
    • CommentTimeFeb 15th 2012
    Has anyone commented already of Ellerman's Adjoint functors and heteromorphisms?
    or other papers about them?
    • CommentRowNumber2.
    • CommentAuthorKevin Watkins
    • CommentTimeFeb 15th 2012

    My intuition is that heteromorphisms (or elements of profunctors, I guess… I’m not an expert) will be important in the syntax of homotopy type theory.

    For example, if Πx:A.B(x)\Pi x:A. B(x) is a dependent product type, and ff is a function of this type, and pp is a path from a 1a_1 to a 2a_2 in AA, then f(p)f(p) is best thought of as a heteropath from f(a 1)f(a_1) to f(a 2)f(a_2). This heteropath is an element of the profunctor B(p)B(p) from B(a 1)B(a_1) to B(a 2)B(a_2).

    Likewise, if Σx:A.B(x)\Sigma x:A. B(x) is a dependent sum type, and pp is a path from (a 1,b 1)(a_1, b_1) to (a 2,b 2)(a_2, b_2) in Σx:A.B(x)\Sigma x:A. B(x), then π 1(p)\pi_1(p) is a path from a 1a_1 to a 2a_2 in AA, and π 2(p)\pi_2(p) is a heteropath from b 1b_1 to b 2b_2 in the profunctor B(p)B(p) from B(a 1)B(a_1) to B(a 2)B(a_2).

    The profunctors that arise would have the special property that they would be representable as functors in both directions. For example B(p)B(p) is representable as a function from B(a 1)B(a_1) to B(a 2)B(a_2), and corepresentable as a function from B(a 2)B(a_2) to B(a 1)B(a_1). For the purposes of homotopy type theory, it might make sense to define an equivalence of types to be such a profunctor. This would seem to be a more symmetrical formulation than Voevodsky’s.

    Speculatively, having a notation for more general profunctors between types, not necessarily equivalences, might allow a nice formulation of some parametricity axioms in homotopy type theory.

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 16th 2012

    That’s an interesting idea, Kevin. I’ve had similar thoughts that it might be useful to work directly with paths “from b 1:B(a 1)b_1\colon B(a_1) to b 2:B(a 2)b_2\colon B(a_2) over p:(a 1=a 2)p\colon (a_1=a_2)” in a direct way, rather than as paths from transport p b1 to b2 the way we currently do. I was more inclined to call them “indexed paths”; they even admit a nice description as an inductive type.

    Inductive ipaths {A} {B : A -> Type} :
      forall (x y : A) (u : B x) (v : B y) (p : x == y), Type :=
    | iidpath : forall (x : A) (u : B x), ipaths x x u u (idpath x).
    
    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeNov 28th 2014

    I have just been alerted of this old thread. Regarding #1: the nnLab does discuss this at Adjoint functors in terms of cographs.

    I am adding pointer there now to a new entry heteromorphism.

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeNov 13th 2015

    David Ellerman kindly informs me by email that he has expanded at heteromorphism

    • CommentRowNumber6.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 24th 2017

    Would I be right in thinking that some regulars here don’t feel too warmly towards the heteromorphism concept. Has double profunctor been enhanced by its inclusion?

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeJun 24th 2017

    I don’t mind the concept, what bothers me is that some heteromorphism people seem to believe there’s something novel or revolutionary about it. The page heteromorphism, for instance, contains the sentence

    The general heteromorphic treatment of adjunctions is due to Pareigis 1970

    which might give the reader the impression that the hom-set-isomorphism definition of adjunctions (which is really all the “heteromorphic treatment” means) is due to Pareigis. (I would fix it but I’m not sure what exactly is being attributed to Pareigis.)

    I think the addition to double profunctor is an improvement; the idea section was rather sparse before.

    • CommentRowNumber8.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 24th 2017

    Thanks. So not inclined to use it for your

    “mixed-category” entailment A[α]CA[\alpha] \vdash C

    • CommentRowNumber9.
    • CommentAuthorThomas Holder
    • CommentTimeJun 24th 2017

    I’ve added a link to Pareigis’ book.

    • CommentRowNumber10.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 24th 2017

    Re #7: my thoughts exactly. The heteromorphism person who added the line about Pareigis’s book is David Ellerman. The thing that seems to go unsaid (or said at most very quietly) in some of the philosophical ruminations I’ve seen is that there is no God-given notion of heteromorphism between categories: any notion of heteromorphism between categories is dependent on a notion of profunctor between categories that one has in mind. So I don’t see a big deal (Ellerman in particular makes much too big a deal of this and how Mac Lane’s treatment of adjoints in Categories for the Working Mathematician could be much improved).