Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
have added this disambiguation line at the very top:
This page is about the notion in homotopy type theory. For parallel transport via connections in differential geometry see there.
It would be helpful if the terminology “transport” here could be qualified, since it is bound to appear with other meanings elsewhere in mathematics and physics (eg. eventually we’ll have a page for transport coefficient, etc.).
How about type transport?
(which would be in line with the analogous issue at type telescope, discussed there.
“type telescope” makes some sense because a telescope of that sort is made up of types. I don’t quite see “type transport” in the same sense. What about maybe “identity transport”? Or, I suppose, “transport (type theory)”?
Maybe even within type theory, you want to leave room for other notions of transport.
(Already in cohesive HoTT there is a type theory version of parallel transport for flat connections.)
Therefore an actual qualification like identity transport would seem useful.
added a remark (here) that identity transport along paths in the shape of a type has the interpretation of parallel transport in the traditional sense.
While I was at it, I gave the “Definition”-section some formatting, and then renamed it to “Idea”, because for the time being there is no definition presented. (Not even a characterization: you might want to add something on composition of transport – I have now at least added the word “compatible” to “there are transport functions”).
added these pointers:
Some more details are spelled out in:
Implementation in Agda:
added the following pointers:
The understanding of transport in HoTT as expressing Leibniz’s principle of “indiscernibility of identicals” (aka “substitution of equals”, “substitutivity”) has been made explicit in:
James Ladyman, Stuart Presnell, §6.3 in: Identity in Homotopy Type Theory, Part I: The Justification of Path Induction, Philosophia Mathematica 23 3 (2015) 386–406 [doi:10.1093/philmat/nkv014, pdf]
Benedikt Ahrens, Paige Randall North, §3.1 in: Univalent foundations and the equivalence principle, in: Reflections on the Foundations of Mathematics, Synthese Library 407 Springer (2019) [arXiv:2202.01892, doi:10.1007/978-3-030-15655-8]
The converse implication of path induction from transport (together with the uniqueness principle for id-types) is made explicit in:
Lennard Götz, §4 in: Martin-Löf’s J-rule, LMU (2018) [pdf]
added pointer to:
as a reference in traditional algebraic topology which explicitly speaks of “transport”.
Anonymouse,
you keep using the word “could” for stating what otherwise seems to be definite claims of yours. Here you say “could be defined”, which sounds like “were it not for” something that prevents this definition – which is probably not what you mean. I think you should write “can be defined” or “may be defined”, for clarity.
1 to 15 of 15