On the understanding of transport in homotopy type theory as expressing Leibniz‘s principle of “indiscernibility of identicals” (aka “substitution of equals” or “substitutivity”), as well as the converse implication of path induction from transport (together with the uniqueness principle for id-types):

- James Ladyman, Stuart Presnell,
*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]

category: people

Last revised on September 23, 2022 at 19:39:43. See the history of this page for a list of all contributions to it.