Notions of anonymous existence in Martin-Löf type theory
DOI10.23638/LMCS-13(1:15)2017zbMATH Open1377.03005arXiv1610.03346MaRDI QIDQ2980980FDOQ2980980
Authors: Nicolai Kraus, Martín Escardo, Thierry Coquand, Thorsten Altenkirch 
Publication date: 8 May 2017
Full work available at URL: https://arxiv.org/abs/1610.03346
Recommendations
truncationfactorizationhomotopy type theorycoherence conditionsanonymous existencebracket typesHedberg's theoremsquash typesweakly constant functions
Logic in computer science (03B70) Categorical logic, topoi (03G30) Functional programming and lambda calculus (68N18)
Cites Work
- Title not available (Why is that?)
- A course in constructive algebra
- Homotopy theoretic models of identity types
- Title not available (Why is that?)
- Axiom of Choice and Complementation
- Title not available (Why is that?)
- Title not available (Why is that?)
- Proof-relevance of families of setoids and identity in type theory
- A coherence theorem for Martin-Löf's type theory
- Generalizations of Hedberg's theorem
- The World's simplest axiom of choice fails
- Propositions as [Types]
- Notions of anonymous existence in Martin-Löf type theory
- The general universal property of the propositional truncation
Cited In (10)
- Type-theoretic approaches to ordinals
- On Small Types in Univalent Foundations
- Univalent categories of modules
- Extensional constructive real analysis via locators
- The justification of identity elimination in Martin-Löf's type theory
- Idempotents in intensional type theory
- Generalizations of Hedberg's theorem
- The Scott model of PCF in univalent type theory
- Notions of anonymous existence in Martin-Löf type theory
- Type theory based semantic verification for service composition in cloud computing environments
Uses Software
This page was built for publication: Notions of anonymous existence in Martin-Löf type theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2980980)
