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]
- Title not available (Why is that?)
- The General Universal Property of the Propositional Truncation
Cited In (7)
- Type-theoretic approaches to ordinals
- On Small Types in Univalent Foundations
- Univalent categories of modules
- Extensional constructive real analysis via locators
- Title not available (Why is that?)
- The Scott model of PCF in univalent 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)
