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

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf sheaves simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

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).
  1. Page created, but author did not leave any comments.


    v1, current

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeMay 21st 2022
    • (edited May 21st 2022)

    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.

    diff, v2, current

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeMay 21st 2022

    “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)”?

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeMay 21st 2022

    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.

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeMay 26th 2022

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

    diff, v3, current

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeSep 3rd 2022

    added these pointers:

    Some more details are spelled out in:

    Implementation in Agda:

    diff, v5, current

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeSep 23rd 2022
    • (edited Sep 23rd 2022)

    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:

    The converse implication of path induction from transport (together with the uniqueness principle for id-types) is made explicit in:

    diff, v7, current

  2. Adding a section on the role transport plays in one definition of univalent Tarski universes, and how that definition is equivalent to the usual definition of univalent universe using the internal types of equivalence and the canonical function idtoequiv


    diff, v9, current

  3. added some syntax for the transport functions


    diff, v14, current

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeOct 16th 2022

    added whitespace to the two formulas in the Idea-section, in order to make it visible how the operators bind

    diff, v15, current

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeJan 18th 2023
    • (edited Jan 18th 2023)

    added pointer to:

    as a reference in traditional algebraic topology which explicitly speaks of “transport”.

    diff, v20, current

  4. Added a definition of transport using Russell universes and function application


    diff, v24, current

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeOct 6th 2023


    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.

  5. could -> can


    diff, v25, current

  6. Added proof that any family of transport functions is a family of equivalences and that the type of families of transport functions is contractible


    diff, v26, current