scientific article; zbMATH DE number 7350774
From MaRDI portal
Publication:4989403
zbMath1498.03037arXiv2002.08150MaRDI QIDQ4989403
Niels van der Weide, Niccolò Veltri
Publication date: 25 May 2021
Full work available at URL: https://arxiv.org/abs/2002.08150
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Abstract and axiomatic homotopy theory in algebraic topology (55U35) 2-categories, bicategories, double categories (18N10) Type theory (03B38)
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
- Two-dimensional monad theory
- Structural induction and coinduction in a fibrational setting
- Inductive families
- A coherent approach to pseudomonads
- Homotopy type theory in Lean
- Towards a directed homotopy type theory
- Weak omega-categories from intensional type theory
- Higher Inductive Types as Homotopy-Initial Algebras
- Type theory in type theory using quotient inductive types
- Biequivalences in tricategories
- π n (S n ) in Homotopy Type Theory
- The Local Universes Model
- Inductive Types in Homotopy Type Theory
- Partiality, Revisited
- Types are weak ω -groupoids
- Displayed Categories
- Inductive-Inductive Definitions
- Homotopy theoretic models of identity types
- A characterization of pie limits
- Quotienting the delay monad by weak bisimilarity
- Cubical Type Theory: a constructive interpretation of the univalence axiom
- Eilenberg-MacLane spaces in homotopy type theory
- A Cubical Approach to Synthetic Homotopy Theory
- Constructions with Non-Recursive Higher Inductive Types
- A Syntax for Higher Inductive-Inductive Types
- Cubical Agda: A dependently typed programming language with univalence and higher inductive types
- The law of excluded middle in the simplicial model of type theory
- A Type-Theoretical Definition of Weak {\omega}-Categories
- The real projective spaces in homotopy type theory
- Impredicative Encodings of (Higher) Inductive Types
- Higher Groups in Homotopy Type Theory
- On Higher Inductive Types in Cubical Type Theory
- Free Higher Groups in Homotopy Type Theory
- The Integers as a Higher Inductive Type
- Constructing Higher Inductive Types as Groupoid Quotients
- Calculating the Fundamental Group of the Circle in Homotopy Type Theory
- Wild omega-Categories for the Homotopy Hypothesis in Type Theory
- Computational higher-dimensional type theory
- Homotopical patch theory
- Homotopy Type Theory: Univalent Foundations of Mathematics
- Univalent categories and the Rezk completion
- Homotopy limits in type theory
This page was built for publication:
