Isomorphism is equality

DOI10.1016/j.indag.2013.09.002zbMath1359.03010OpenAlexW2039140273MaRDI QIDQ740487

Nils Anders Danielsson, Thierry Coquand

Publication date: 3 September 2014

Published in: Indagationes Mathematicae. New Series (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.indag.2013.09.002

zbMATH Keywords

univalenceproof assistantsdependent type theory

Mathematics Subject Classification ID

Related Items (7)

Observability in the univalent universe ⋮ Univalent Foundations and the Equivalence Principle ⋮ Univalent Foundations and the UniMath Library ⋮ Displayed Categories ⋮ Univalent categories and the Rezk completion ⋮ Unnamed Item ⋮ Cubical Agda: A dependently typed programming language with univalence and higher inductive types

Uses Software

• Coq
• Automath
• Agda
• GitHub

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Telescopic mappings in typed lambda calculus
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• Univalent Foundations of Mathematics
• Homotopy theoretic models of identity types
• What are logical notions?
• Sentences of type theory: the only sentences preserved under isomorphisms
• A coherence theorem for Martin-Löf's type theory
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Univalent categories and the Rezk completion

This page was built for publication: Isomorphism is equality