scientific article
From MaRDI portal
Publication:2968413
DOI10.4230/LIPIcs.TYPES.2013.107zbMath1359.03009MaRDI QIDQ2968413
Thierry Coquand, Marc Bezem, Simon Huber
Publication date: 13 March 2017
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items (62)
Varieties of Cubical Sets ⋮ Adjoint Logic with a 2-Category of Modes ⋮ Finitary higher inductive types in the groupoid model ⋮ The construction of set-truncated higher inductive types ⋮ Homotopical patch theory ⋮ Games for Dependent Types ⋮ Cubical methods in homotopy type theory and univalent foundations ⋮ Naive cubical type theory ⋮ Game semantics for dependent types ⋮ Proof-Relevant Parametricity ⋮ Languages of higher-dimensional automata ⋮ Parametric Polymorphism — Universally ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Meaning explanations at higher dimension ⋮ Higher Structures in Homotopy Type Theory ⋮ Rensets and renaming-based recursion for syntax with bindings extended version ⋮ Martin-Löf identity types in C-systems ⋮ Two-level type theory and applications ⋮ Canonicity and homotopy canonicity for cubical type theory ⋮ Towards a constructive simplicial model of Univalent Foundations ⋮ Univalent foundations as structuralist foundations ⋮ Eliminating dependent pattern matching without K ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Universal properties for universal types in bifibrational parametricity ⋮ A presheaf model of parametric type theory ⋮ Bifibrational functorial semantics of parametric polymorphism ⋮ Unnamed Item ⋮ Denotational semantics for guarded dependent type theory ⋮ Cubical $(\omega,p)$-categories ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017 ⋮ Constructing a universe for the setoid model ⋮ From Mathesis Universalis to Provability, Computability, and Constructivity ⋮ Unnamed Item ⋮ A Kripke model for simplicial sets ⋮ The Frobenius condition, right properness, and uniform fibrations ⋮ Cubical Type Theory: a constructive interpretation of the univalence axiom ⋮ Unnamed Item ⋮ Unnamed Item ⋮ An introduction to univalent foundations for mathematicians ⋮ Unnamed Item ⋮ Combinatorial topology and constructive mathematics ⋮ A cubical model of homotopy type theory ⋮ Proof Theory of Constructive Systems: Inductive Types and Univalence ⋮ Cartesian cubical computational type theory: Constructive reasoning with paths and equalities ⋮ A meaning explanation for HoTT ⋮ Some Wellfounded Trees in UniMath ⋮ The univalence axiom in cubical sets ⋮ Canonicity for cubical type theory ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Towards a Cubical Type Theory without an Interval ⋮ UNIVERSES AND UNIVALENCE IN HOMOTOPY TYPE THEORY ⋮ Functional Kan Simplicial Sets: Non-Constructivity of Exponentiation ⋮ Models of Type Theory Based on Moore Paths ⋮ A homotopy-theoretic model of function extensionality in the effective topos ⋮ Natural models of homotopy type theory ⋮ Rensets and renaming-based recursion for syntax with bindings ⋮ Model structure on the universe of all types in interval type theory ⋮ Syntax and models of Cartesian cubical type theory
This page was built for publication:
