10 found
Order:
  1.  61
    Identity in Homotopy Type Theory, Part I: The Justification of Path Induction.James Ladyman & Stuart Presnell - 2015 - Philosophia Mathematica 23 (3):386-406.
    Homotopy Type Theory is a proposed new language and foundation for mathematics, combining algebraic topology with logic. An important rule for the treatment of identity in HoTT is path induction, which is commonly explained by appeal to the homotopy interpretation of the theory's types, tokens, and identities as spaces, points, and paths. However, if HoTT is to be an autonomous foundation then such an interpretation cannot play a fundamental role. In this paper we give a derivation of path induction, motivated (...)
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography   5 citations  
  2.  62
    Does Homotopy Type Theory Provide a Foundation for Mathematics?James Ladyman & Stuart Presnell - forthcoming - British Journal for the Philosophy of Science:axw006.
    Homotopy Type Theory is a putative new foundation for mathematics grounded in constructive intensional type theory that offers an alternative to the foundations provided by ZFC set theory and category theory. This article explains and motivates an account of how to define, justify, and think about HoTT in a way that is self-contained, and argues that, so construed, it is a candidate for being an autonomous foundation for mathematics. We first consider various questions that a foundation for mathematics might be (...)
    Direct download (7 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  3. The Connection Between Logical and Thermodynamic Irreversibility.James Ladyman, Stuart Presnell, Anthony J. Short & Berry Groisman - 2007 - Studies in History and Philosophy of Science Part B: Studies in History and Philosophy of Modern Physics 38 (1):58-79.
    There has recently been a good deal of controversy about Landauer's Principle, which is often stated as follows: The erasure of one bit of information in a computational device is necessarily accompanied by a generation of kTln2 heat. This is often generalised to the claim that any logically irreversible operation cannot be implemented in a thermodynamically reversible way. John Norton (2005) and Owen Maroney (2005) both argue that Landauer's Principle has not been shown to hold in general, and Maroney offers (...)
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography   6 citations  
  4. The Use of the Information-Theoretic Entropy in Thermodynamics.James Ladyman, Stuart Presnell & Anthony J. Short - 2008 - Studies in History and Philosophy of Science Part B: Studies in History and Philosophy of Modern Physics 39 (2):315-324.
    When considering controversial thermodynamic scenarios such as Maxwell's demon, it is often necessary to consider probabilistic mixtures of states. This raises the question of how, if at all, to assign entropy to them. The information-theoretic entropy is often used in such cases; however, no general proof of the soundness of doing so has been given, and indeed some arguments against doing so have been presented. We offer a general proof of the applicability of the information-theoretic entropy to probabilistic mixtures of (...)
    Direct download (7 more)  
     
    Export citation  
     
    My bibliography   4 citations  
  5.  24
    Identity in Homotopy Type Theory: Part II, The Conceptual and Philosophical Status of Identity in HoTT.James Ladyman & Stuart Presnell - forthcoming - Philosophia Mathematica:nkw023.
    Among the most interesting features of Homotopy Type Theory is the way it treats identity, which has various unusual characteristics. We examine the formal features of “identity types” in HoTT, and how they relate to its other features including intensionality, constructive logic, the interpretation of types as concepts, and the Univalence Axiom. The unusual behaviour of identity types might suggest that they be reinterpreted as representing indiscernibility. We explore this by defining indiscernibility in HoTT and examine its relationship with identity. (...)
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  6.  58
    The Connection Between Logical and Thermodynamical Irreversibility.Tony Short, James Ladyman, Berry Groisman & Stuart Presnell - unknown
    There has recently been a good deal of controversy about Landauer's Principle, which is often stated as follows: The erasure of one bit of information in a computational device is necessarily accompanied by a generation of kT ln 2 heat. This is often generalised to the claim that any logically irreversible operation cannot be implemented in a thermodynamically reversible way. John Norton (2005) and Owen Maroney (2005) both argue that Landauer's Principle has not been shown to hold in general, and (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  7.  3
    The Use of the Information-Theoretic Entropy in Thermodynamics.James Ladyman, Stuart Presnell & Anthony J. Short - 2008 - Studies in History and Philosophy of Science Part B: Studies in History and Philosophy of Modern Physics 39 (2):315-324.
  8.  4
    The Connection Between Logical and Thermodynamic Irreversibility.James Ladyman, Stuart Presnell, Anthony J. Short & Berry Groisman - 2007 - Studies in History and Philosophy of Science Part B: Studies in History and Philosophy of Modern Physics 38 (1):58-79.
  9.  35
    A Primer on Homotopy Type Theory Part 1: The Formal Type Theory.James Ladyman & Stuart Presnell - unknown
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  10.  29
    Identity in HoTT, Part I.James Ladyman & Stuart Presnell - unknown
    Homotopy type theory is a new branch of mathematics that connects algebraic topology with logic and computer science, and which has been proposed as a new language and conceptual framework for math- ematical practice. Much of the power of HoTT lies in the correspondence between the formal type theory and ideas from homotopy theory, in par- ticular the interpretation of types, tokens, and equalities as spaces, points, and paths. Fundamental to the use of identity and equality in HoTT is the (...)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography