## Not signed in

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

## Discussion Tag Cloud

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

• CommentRowNumber1.
• CommentAuthorjim_stasheff
• CommentTimeFeb 15th 2012
• 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 $\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.

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

• CommentRowNumber4.
• CommentAuthorUrs
• CommentTimeNov 28th 2014

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.

• 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[\alpha] \vdash C$

• CommentRowNumber9.
• CommentAuthorThomas Holder
• CommentTimeJun 24th 2017