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.
   • CommentAuthorjim_stasheff
   • CommentTimeFeb 15th 2012
   • PermaLink
   Author: jim_stasheff
   Format: TextHas anyone commented already of Ellerman's Adjoint functors and heteromorphisms? or other papers about them?

   Has anyone commented already of Ellerman's Adjoint functors and heteromorphisms?
   or other papers about them?
2. • CommentRowNumber2.
   • CommentAuthorKevin Watkins
   • CommentTimeFeb 15th 2012
   • PermaLink
   Author: Kevin Watkins
   Format: MarkdownItexMy 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 $\Pi x:A. B(x)$ is a dependent product type, and $f$ is a function of this type, and $p$ is a path from $a_1$ to $a_2$ in $A$, then $f(p)$ is best thought of as a heteropath from $f(a_1)$ to $f(a_2)$. This heteropath is an element of the profunctor $B(p)$ from $B(a_1)$ to $B(a_2)$. Likewise, if $\Sigma x:A. B(x)$ is a dependent sum type, and $p$ is a path from $(a_1, b_1)$ to $(a_2, b_2)$ in $\Sigma x:A. B(x)$, then $\pi_1(p)$ is a path from $a_1$ to $a_2$ in $A$, and $\pi_2(p)$ is a heteropath from $b_1$ to $b_2$ in the profunctor $B(p)$ from $B(a_1)$ to $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)$ is representable as a function from $B(a_1)$ to $B(a_2)$, and corepresentable as a function from $B(a_2)$ to $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.

   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 $\Pi x:A. B(x)$ is a dependent product type, and $f$ is a function of this type, and $p$ is a path from $a_1$ to $a_2$ in $A$, then $f(p)$ is best thought of as a heteropath from $f(a_1)$ to $f(a_2)$. This heteropath is an element of the profunctor $B(p)$ from $B(a_1)$ to $B(a_2)$.

   Likewise, if $\Sigma x:A. B(x)$ is a dependent sum type, and $p$ is a path from $(a_1, b_1)$ to $(a_2, b_2)$ in $\Sigma x:A. B(x)$, then $\pi_1(p)$ is a path from $a_1$ to $a_2$ in $A$, and $\pi_2(p)$ is a heteropath from $b_1$ to $b_2$ in the profunctor $B(p)$ from $B(a_1)$ to $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)$ is representable as a function from $B(a_1)$ to $B(a_2)$, and corepresentable as a function from $B(a_2)$ to $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.

3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeFeb 16th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThat's an interesting idea, Kevin. I've had similar thoughts that it might be useful to work directly with paths "from $b_1\colon B(a_1)$ to $b_2\colon B(a_2)$ over $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).

   That’s an interesting idea, Kevin. I’ve had similar thoughts that it might be useful to work directly with paths “from $b_1\colon B(a_1)$ to $b_2\colon B(a_2)$ over $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).
   

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeNov 28th 2014
   • PermaLink
   Author: Urs
   Format: MarkdownItexI have just been alerted of this old thread. Regarding #1: the $n$Lab does discuss this at _[Adjoint functors in terms of cographs](cograph+of+a+functor#AdjointFunctorsInTermsOfCographs)_. I am adding pointer there now to a new entry [[heteromorphism]].

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

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

5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeNov 13th 2015
   • PermaLink
   Author: Urs
   Format: MarkdownItexDavid Ellerman kindly informs me by email that he has expanded at _[[heteromorphism]]_

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

6. • CommentRowNumber6.
   • CommentAuthorDavid_Corfield
   • CommentTimeJun 24th 2017
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexWould 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?

   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?

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeJun 24th 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI 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.

   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.

8. • CommentRowNumber8.
   • CommentAuthorDavid_Corfield
   • CommentTimeJun 24th 2017
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexThanks. So not inclined to use it for [your](http://dlicata.web.wesleyan.edu/pubs/ls15adjoint/ls15adjoint.pdf) >"mixed-category" entailment $A[\alpha] \vdash C$

   Thanks. So not inclined to use it for your

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

9. • CommentRowNumber9.
   • CommentAuthorThomas Holder
   • CommentTimeJun 24th 2017
   • PermaLink
   Author: Thomas Holder
   Format: MarkdownItexI've added a link to Pareigis' book.

   I’ve added a link to Pareigis’ book.

10. • CommentRowNumber10.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 24th 2017
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexRe #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).

    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).