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):
Last revised on September 23, 2022 at 19:41:07. See the history of this page for a list of all contributions to it.