Notions of anonymous existence in Martin-Löf type theory

QR Code

Notions of anonymous existence in Martin-Löf 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...

Full description

Bibliographic Details
Main Authors:	Kraus, Nicolai, Escardo, Martin, Coquand, Thierry, Altenkirch, Thorsten
Format:	Article
Published:	IfCoLog 2016
Subjects:	homotopy type theory Hedberg’s theorem anonymous existence weakly constant functions factorization truncation squash types bracket types coherence conditions
Online Access:	https://eprints.nottingham.ac.uk/38092/

Similar Items

Extending homotopy type theory with strict equality
by: Altenkirch, Thorsten, et al.
Published: (2016)

Truncation levels in homotopy type theory
by: Kraus, Nicolai
Published: (2015)

Constructions with non-recursive higher inductive types
by: Kraus, Nicolai
Published: (2016)

Partiality, revisited: the partiality monad as a quotient inductive-inductive type
by: Altenkirch, Thorsten, et al.
Published: (2017)

Towards a cubical type theory without an interval
by: Altenkirch, Thorsten, et al.
Published: (2017)

Type theory in type theory using quotient inductive types
by: Altenkirch, Thorsten, et al.
Published: (2016)

Quotient types in type theory
by: Li, Nuo
Published: (2015)

Univalent higher categories via complete semi-segal types
by: Capriotti, Paolo, et al.
Published: (2018)

Higher inductive types, inductive families, and inductive-inductive types
by: von Raumer, Jakob
Published: (2020)

Type theory in a type theory with quotient inductive types
by: Kaposi, Ambrus
Published: (2017)

Types with extra structure: predicates, equations, composition
by: Hewer, Brandon
Published: (2024)

Normalisation by evaluation for dependent types
by: Altenkirch, Thorsten, et al.
Published: (2016)

Normalisation by evaluation for type theory, in type theory
by: Altenkirch, Thorsten, et al.
Published: (2017)

The existence of global weak solutions for a weakly dissipative Camassa-Holm equation in H1(R)
by: Lai, S., et al.
Published: (2013)

Baroque Historical Dances Lecture and Workshop by Mireia Frutos Fernandez : World Music History Lecture Series
by: Universiti Teknologi MARA, Faculty of Music
Published: (2018)

The worth of anonymous feedback
by: Dreher, Heinz, et al.
Published: (2006)

The Common Law and Taxation of Trusts in Australia in the Twenty-First Century
by: Fullarton, Alexander
Published: (2007)

Analysis of g s-transferase, protien tyrosine phosphatase 1B, nuclear factor kappa-B1 and leptin receptor genetic polymorphisms as risk factors for Malaysian type 2 diabetes mellitus subjects
by: Etemad, Ali
Published: (2013)

Get rid of yourself: toward an aesthetics of anonymity
by: Eckersley, David
Published: (2019)

Influence of vegetation and soil types on the wheatbelt termite, Drepanotermes tamminensis (Hill), in the Western Australian wheatbelt
by: Park, H., et al.
Published: (1994)

Anonymous: a social movement
by: Knight, William
Published: (2018)

Anonymous feedback in e-learning systems
by: Dreher, Heinz
Published: (2005)

Existence and uniqueness of solutions for nonlocal p-Laplacian problems
by: Behrouz, Emamizadeh, et al.
Published: (2016)

Getting goose bumps about teaching evolution
by: Foster, Colin
Published: (2014)

A Study on Relationship Between Decision-making Behaviour and Myers-Briggs Type Indicator
by: Chen, Jelico
Published: (2007)

Determining the factors affecting consumer’s purchase intention towards foreign brands among the y-generation in the northern area of Malaysia / Etty Harniza Harun, Mahazir Ismail, Nur Aizureen Anwar
by: Harun, Etty Harniza, et al.
Published: (2014)

تعليم العربية من خلال الشعر الإسلامي لطلاّب المستوى المتقدِّم غير الناطقين بها: دراسة وصفية وتحليلية = Teaching Arabic to non-native speakers through Islamic poetry for advanced level students
by: Mohamed, Esameldien Dafalla
Published: (2013)

مناهج مقترحة لتعليم التعبيرات الاصطلاحية للناطقين بغير العربية
by: Yousuf, Mohamed Abdel Rahman Ibrahim
Published: (2011)

Identifying personality traits in Oman high schol students: a test for big five-factor model / Muna Saif Abdullah Al-Kalbani
by: Abdullah Al-Kalbani, Muna Saif
Published: (2010)

Factors associated with glycaemic control among diabetes mellitus type 2 patients attending health clinics in Tampin district Negeri Sembilan, Malaysia
by: Wan Hamdzan, Wan Farzana Fasya
Published: (2016)

Supermonads: one notion to bind them all
by: Bracker, Jan, et al.
Published: (2016)

Association of dietary patterns with socio-demographic, lifestyle, weight status and biochemical profiles among type 2 diabetes mellitus patients in a special Medical Center, Tehran Iran
by: Zad, Nasrin Darani
Published: (2012)

Practical fair anonymous undeniable signatures
by: Han, Song, et al.
Published: (2004)

On Nie-Tan operator and type-reduction of interval type-2 fuzzy sets
by: Li, Jiawei, et al.
Published: (2018)

Study of bandgap property of a bilayer membrane-type metamaterial applied on a thin plate
by: GAO, Cong, et al.
Published: (2020)

Iron Formation: The Sedimentary Product of a Complex Interplay among Mantle, Tectonic, Oceanic, and Biospheric Processes
by: Bekker, A., et al.
Published: (2010)

The role of C-type lectin receptors in the recognition of Pseudiminas aeruginosa
by: Alshahrani, Mohammad
Published: (2018)

Core self-evaluations, job satisfaction, transformational and servant leadership model in the Roman Catholic education system / Ginavee F. Dapula and Mary Caroline N. Castano
by: Dapula, Ginavee F., et al.
Published: (2017)

Investigating readiness of virtual classroom environment (VCE) among students / Wan Abdul Rahim Wan Mohd Isa, Vivi Noryati Ahmad and Dg Asnani Ag Nordin
by: Wan Mohd Isa, Wan Abdul Rahim, et al.
Published: (2018)

Which form of assessment provides the best information about student performance in chemistry examinations?
by: Hudson, R., et al.
Published: (2013)