scientific article; zbMATH DE number 7168146
From MaRDI portal
Publication:5216301
Publication date: 17 February 2020
Full work available at URL: https://arxiv.org/abs/1902.00297
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items (2)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Logical relations and parametricity -- a Reynolds programme for category theory and programming languages
- Canonicity of weak \(\omega\)-groupoid laws using parametricity theory
- Generalized algebraic theories and contextual categories
- Inductive families
- Quotient inductive-inductive types
- Finitary higher inductive types in the groupoid model
- Containers: Constructing strictly positive types
- Higher Inductive Types as Homotopy-Initial Algebras
- Type theory in type theory using quotient inductive types
- Proofs for free
- Positive Inductive-Recursive Definitions
- A type theory for synthetic $\infty$-categories
- Two-dimensional models of type theory
- A coherence theorem for Martin-Löf's type theory
- A general formulation of simultaneous inductive-recursive definitions in type theory
- Cubical Type Theory: a constructive interpretation of the univalence axiom
- Type Theory based on Dependent Inductive and Coinductive Types
- Constructions with Non-Recursive Higher Inductive Types
- Internal type theory
- Semantics of higher inductive types
- A Syntax for Higher Inductive-Inductive Types
- On Higher Inductive Types in Cubical Type Theory
- Free Higher Groups in Homotopy Type Theory
- Constructing Higher Inductive Types as Groupoid Quotients
- Parametricity and dependent types
- Indexed containers
- A relationally parametric model of dependent type theory
- Homotopy Type Theory: Univalent Foundations of Mathematics
- Univalent categories and the Rezk completion
This page was built for publication:
