scientific article

DOI10.23638/LMCS-13(1:15)2017zbMath1377.03005arXiv1610.03346MaRDI QIDQ2980980

Martín Hötzel Escardó, Nicolai Kraus, Thierry Coquand, Thorsten Altenkirch

Publication date: 8 May 2017

Full work available at URL: https://arxiv.org/abs/1610.03346

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

truncationfactorizationhomotopy type theorycoherence conditionsanonymous existencebracket typesHedberg's theoremsquash typesweakly constant functions

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Categorical logic, topoi (03G30)

Related Items (7)

Unnamed Item ⋮ The Scott model of PCF in univalent type theory ⋮ On Small Types in Univalent Foundations ⋮ Univalent categories of modules ⋮ Type theory based semantic verification for service composition in cloud computing environments ⋮ Type-theoretic approaches to ordinals ⋮ Extensional constructive real analysis via locators

Uses Software

• GitHub

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proof-relevance of families of setoids and identity in type theory
• The World's simplest axiom of choice fails
• A course in constructive algebra
• Homotopy theoretic models of identity types
• Axiom of Choice and Complementation
• A coherence theorem for Martin-Löf's type theory
• Propositions as [Types]
• The General Universal Property of the Propositional Truncation
• Generalizations of Hedberg’s Theorem

This page was built for publication: