Isomorphism is equality
type: Item
instance of: scholarly article
title: Isomorphism is equality
zbMATH Open document ID: 1359.03010
author: Thierry Coquand
author: Nils Anders Danielsson
published in: Indagationes Mathematicae. New Series
publication date: 2014-09-03T00:00:00Z
Mathematics Subject Classification ID: 03B15
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 20M99
Mathematics Subject Classification ID: 08A99
zbMATH DE Number: 6339335
zbMATH Keywords: dependent type theory
zbMATH Keywords: proof assistants
zbMATH Keywords: univalence
describes a project that uses: Coq
describes a project that uses: Automath
describes a project that uses: Agda
describes a project that uses: GitHub
MaRDI profile type: Publication
full work available at URL: j.indag.2013.09.002
OpenAlex ID: W2039140273
cites work: Univalent categories and the Rezk completion
cites work: Homotopy theoretic models of identity types
cites work: Q3754620
cites work: Telescopic mappings in typed lambda calculus
cites work: Q4055619
cites work: A coherence theorem for Martin-Löf's type theory
cites work: Q4247303
cites work: Sentences of type theory: the only sentences preserved under isomorphisms
cites work: Q4099613
cites work: Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
cites work: Q3999860
cites work: What are logical notions?
cites work: Homotopy Type Theory: Univalent Foundations of Mathematics
cites work: Univalent Foundations of Mathematics
cites work: Q3877069
DOI: 10.1016/J.INDAG.2013.09.002
description: scientific article; zbMATH DE number 6339335