Constructing higher inductive types as groupoid quotients

zbMATH Open1498.03037arXiv2002.08150MaRDI QIDQ4989403FDOQ4989403

Authors: Niccolò Veltri, Niels van der Weide 

Publication date: 25 May 2021

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

Recommendations

• Constructing higher inductive types as groupoid quotients
• Quotient inductive-inductive types
• Semantics of higher inductive types
• Higher inductive types as homotopy-initial algebras
• Quotients, inductive types, and quotient inductive types

zbMATH Keywords

Coqbicategorieshomotopy type theoryhigher inductive types

Mathematics Subject Classification ID

Abstract and axiomatic homotopy theory in algebraic topology (55U35) 2-categories, bicategories, double categories (18N10) Type theory (03B38)

Cites Work

• Structural induction and coinduction in a fibrational setting
• Title not available (Why is that?)
• Title not available (Why is that?)
• Two-dimensional monad theory
• Inductive families
• Types are weak \(\omega \)-groupoids
• Homotopy theoretic models of identity types
• Title not available (Why is that?)
• Homotopy type theory. Univalent foundations of mathematics
• Title not available (Why is that?)
• Weak omega-categories from intensional type theory
• A coherent approach to pseudomonads
• The local universes model: an overlooked coherence construction for dependent type theories
• The law of excluded middle in the simplicial model of type theory
• Univalent categories and the Rezk completion
• Biequivalences in tricategories
• A characterization of pie limits
• Inductive-inductive definitions
• A cubical approach to synthetic homotopy theory
• A syntax for higher inductive-inductive types
• Computational higher-dimensional type theory
• Homotopy limits in type theory
• Inductive types in homotopy type theory
• Constructions with non-recursive higher inductive types
• Constructing higher inductive types as groupoid quotients
• Title not available (Why is that?)
• A Type-Theoretical Definition of Weak {\omega}-Categories
• Title not available (Why is that?)
• Homotopy type theory in Lean
• Cubical type theory: a constructive interpretation of the univalence axiom
• Wild \(\omega\)-categories for the homotopy hypothesis in type theory
• Higher inductive types as homotopy-initial algebras
• Eilenberg-MacLane spaces in homotopy type theory
• The real projective spaces in homotopy type theory
• Towards a directed homotopy type theory
• Type theory in type theory using quotient inductive types
• Partiality, Revisited
• Displayed categories
• Quotienting the delay monad by weak bisimilarity
• A syntactical approach to weak omega-groupoids
• On higher inductive types in cubical type theory
• Calculating the Fundamental Group of the Circle in Homotopy Type Theory
• Normalisation by evaluation for type theory, in type theory
• Homotopical patch theory
• Higher groups in homotopy type theory
• Free higher groups in homotopy type theory
• Cubical Agda: a dependently typed programming language with univalence and higher inductive types
• \(\pi _{n }(S ^{n })\) in homotopy type theory
• A finite axiomatisation of inductive-inductive definitions
• Impredicative encodings of (higher) inductive types
• Title not available (Why is that?)
• The integers as a higher inductive type

Cited In (7)

• Topological quantum gates in homotopy type theory
• Bicategories in univalent foundations
• Free higher groups in homotopy type theory
• A construction method for induced types and its application to \(G_2\)
• Semantics of higher inductive types
• Constructions with non-recursive higher inductive types
• Constructing higher inductive types as groupoid quotients

Uses Software

• Coq
• cubicaltt
• Cubical agda

This page was built for publication: Constructing higher inductive types as groupoid quotients

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4989403)