scientific article; zbMATH DE number 7566056
From MaRDI portal
Publication:5094128
Daniel Gratzer, Jonathan Sterling, Carlo Angiuli
Publication date: 2 August 2022
Full work available at URL: https://arxiv.org/abs/2003.01491
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory
- Relating first-order set theories, toposes and categories of classes
- Programming with algebraic effects and handlers
- Generalized algebraic theories and contextual categories
- Constructivism in mathematics. An introduction. Volume I
- Constructing type systems over an operational semantics
- A cubical model of homotopy type theory
- An algorithm for type-checking dependent types
- The simplicial model of univalent foundations (after Voevodsky)
- Setoid type theory -- a syntactic translation
- A Kripke model for simplicial sets
- Homotopy theory of simplicial sheaves in completely decomposable topologies
- Canonicity for cubical type theory
- Type theory and formalisation of mathematics
- Canonicity and normalization for dependent type theory
- Weak omega-categories from intensional type theory
- Programming up to Congruence
- Type theory in type theory using quotient inductive types
- On Irrelevance and Algorithmic Equality in Predicative Type Theory
- Homotopy Type Theory
- Subsystems and regular quotients of C-systems
- Types are weak ω -groupoids
- A type theory for synthetic $\infty$-categories
- Natural models of homotopy type theory
- Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory
- Homotopy theoretic models of identity types
- A Brief Introduction to Algebraic Set Theory
- A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance
- The Type Theory of PL/CV3
- A framework for defining logics
- Cubical Type Theory: a constructive interpretation of the univalence axiom
- Goodwillie's calculus of functors and higher topos theory
- Propositions as [Types]
- Connected limits, familial representability and Artin glueing
- Cubical Agda: A dependently typed programming language with univalence and higher inductive types
- Logical Relations as Types: Proof-Relevant Parametricity for Program Modules
- Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
- Pointers in Recursion: Exploring the Tropics
- A generalized Blakers–Massey theorem
- Fibred Fibration Categories
- Topo-logie
- Deciding type equivalence in a language with singleton kinds
- A Verified Theorem Prover Backend Supported by a Monotonic Library
- On equivalence and canonical forms in the LF type theory
- Extensional equivalence and singleton types
- Normalisation by Evaluation for Dependent Types.
- Computational higher-dimensional type theory
- Homotopy Type Theory: Univalent Foundations of Mathematics
- Higher Topos Theory (AM-170)
- Intensional interpretations of functionals of finite type I
- FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES
- The biequivalence of locally cartesian closed categories and Martin-Löf type theories
- Univalence for inverse diagrams and homotopy canonicity
- The univalence axiom for elegant Reedy presheaves
This page was built for publication:
