Notions of Anonymous Existence in Martin-L\"of Type Theory

As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-L\"of type theory cannot generally be shown to be unique. Inspired by a theorem by Hedberg, we give some simple characterizations of types that do have unique identity proofs. A key ingredient in these const...

תיאור מלא

מידע ביבליוגרפי

Principais autores:	Nicolai Kraus, Martín Escardó, Thierry Coquand, Thorsten Altenkirch
פורמט:	Artigo
שפה:	Inglês
יצא לאור:	Logical Methods in Computer Science e.V. 2017-03-01
סדרה:	Logical Methods in Computer Science
נושאים:	computer science - logic in computer science 03b15 f.4.1
גישה מקוונת:	https://lmcs.episciences.org/3217/pdf
תגים:	הוספת תג אין תגיות, היה/י הראשונ/ה לתייג את הרשומה!