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
• 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
• Title not available (Why is that?)
• On Higher Inductive Types in Cubical Type Theory
• Calculating the Fundamental Group of the Circle in Homotopy Type Theory
• Title not available (Why is that?)
• 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
• π n (S n ) in Homotopy Type Theory
• Title not available (Why is that?)
• Impredicative Encodings of (Higher) Inductive Types
• Title not available (Why is that?)
• The Integers as a Higher Inductive Type

Cited In (3)

• Topological quantum gates in homotopy type theory
• Bicategories in univalent foundations
• A construction method for induced types and its application to \(G_2\)

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)