The Justification of Identity Elimination in Martin-Löf's Type Theory.

On the basis of Martin-Löf's meaning explanations for his type theory a detailed justification is offered of the rule of identity elimination. Brief discussions are thereafter offered of how the univalence axiom fares with respect to these meaning explanations and of some recent work on identity in...

Descripción completa

Detalles Bibliográficos
Publicado en:Topoi: An International Review of Philosophy Vol. 38; no. 3; pp. 577 - 591
Autor principal: Klev, Ansten
Formato: Artículo
Publicado: Springer Nature Sep2019
Materias:
Acceso en línea:Ver este registro en EBSCOhost
fields @attributes:
  recordID: 1
pdfLink:
plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=138029917&site=ehost-live
header:
  @attributes:
    shortDbName: hlh
    uiTerm: 138029917
    longDbName: Humanities International Complete
    uiTag: AN
  controlInfo:
    bkinfo:
    jinfo:
      jid:
        01677411
        NM2
      jtl: Topoi: An International Review of Philosophy
      issn: 01677411
      maglogo: N
    pubinfo:
      dt: Sep2019
      vid: 38
      iid: 3
      pid: 237
      pub: Springer Nature
    artinfo:
      ui:
        138029917
        10.1007/s11245-017-9509-1
      ppf: 577
      ppct: 14
      formats:
        fmt:
          – @attributes:
              type: T
          – @attributes:
              type: P
              size: 2.9MB
      tig:
        atl: The Justification of Identity Elimination in Martin-Löf's Type Theory.
      aug:
        au: Klev, Ansten
        affil: Department of Logic, Institute of Philosophy, Czech Academy of Sciences, Jilská 1, 110 00, Praha 1, Czech Republic
      su:
        Legal justification
        Axioms
      sug:
        subj:
          Legal justification
          Axioms
      keyword:
        Identity
        Justification of logical laws
        Type theory
      ab: On the basis of Martin-Löf's meaning explanations for his type theory a detailed justification is offered of the rule of identity elimination. Brief discussions are thereafter offered of how the univalence axiom fares with respect to these meaning explanations and of some recent work on identity in type theory by Ladyman and Presnell.
      pubtype: Academic Journal
      doctype: Article
      src: R
    language: English
    refInfo:
    copyright:
      @attributes:
        flag: Y
      custom: Topoi: An International Review of Philosophy is a copyright of Springer, 2019. All Rights Reserved.
      item: Topoi: An International Review of Philosophy
      holder: Springer Nature
      dt:
        @attributes:
          year: 2019
    holdings:
      @attributes:
        islocal: N