Ladyman, James and Presnell, Stuart. 2015. “Identity in Homotopy Type Theory, Part I: The Justification of Path Induction.”Philosophia Mathematica 23(3): 386–406.
Ladyman, James and Presnell, Stuart. 2017. “Identity in Homotopy Type Theory: Part II, The Conceptual and Philosophical Status of Identity in HoTT.”Philosophia Mathematica 25(2): 210–245.