Constructing higher inductive types as groupoid quotients
From MaRDI portal
Recommendations
Cites work
- \(\pi _{n }(S ^{n })\) in homotopy type theory
- A characterization of pie limits
- A coherent approach to pseudomonads
- A cubical approach to synthetic homotopy theory
- A finite axiomatisation of inductive-inductive definitions
- A syntactical approach to weak omega-groupoids
- A syntax for higher inductive-inductive types
- A Type-Theoretical Definition of Weak {\omega}-Categories
- Biequivalences in tricategories
- Calculating the Fundamental Group of the Circle in Homotopy Type Theory
- Computational higher-dimensional type theory
- Constructing higher inductive types as groupoid quotients
- Constructions with non-recursive higher inductive types
- Cubical Agda: a dependently typed programming language with univalence and higher inductive types
- Cubical type theory: a constructive interpretation of the univalence axiom
- Displayed categories
- Eilenberg-MacLane spaces in homotopy type theory
- Free higher groups in homotopy type theory
- Higher groups in homotopy type theory
- Higher inductive types as homotopy-initial algebras
- Homotopical patch theory
- Homotopy canonicity for cubical type theory
- Homotopy limits in type theory
- Homotopy theoretic models of identity types
- Homotopy type theory in Lean
- Homotopy type theory. Univalent foundations of mathematics
- scientific article; zbMATH DE number 6694181 (Why is no real title available?)
- scientific article; zbMATH DE number 2125652 (Why is no real title available?)
- scientific article; zbMATH DE number 3521950 (Why is no real title available?)
- scientific article; zbMATH DE number 1302059 (Why is no real title available?)
- scientific article; zbMATH DE number 1342277 (Why is no real title available?)
- scientific article; zbMATH DE number 1956503 (Why is no real title available?)
- Impredicative encodings of (higher) inductive types
- Inductive families
- Inductive types in homotopy type theory
- Inductive-inductive definitions
- Normalisation by evaluation for type theory, in type theory
- On higher inductive types in cubical type theory
- Partiality, Revisited
- Quotienting the delay monad by weak bisimilarity
- Structural induction and coinduction in a fibrational setting
- The integers as a higher inductive type
- The law of excluded middle in the simplicial model of type theory
- The local universes model: an overlooked coherence construction for dependent type theories
- The real projective spaces in homotopy type theory
- Towards a directed homotopy type theory
- Two-dimensional monad theory
- Type theory in type theory using quotient inductive types
- Types are weak -groupoids
- Univalent categories and the Rezk completion
- Weak omega-categories from intensional type theory
- Wild \(\omega\)-categories for the homotopy hypothesis in type theory
Cited in
(11)- A construction method for induced types and its application to G₂
- Finitary higher inductive types in the groupoid model
- The construction of set-truncated higher inductive types
- Constructions with non-recursive higher inductive types
- Semantics of higher inductive types
- Bicategories in univalent foundations
- Free higher groups in homotopy type theory
- Constructing higher inductive types as groupoid quotients
- Topological quantum gates in homotopy type theory
- The formal theory of monads, univalently
- Univalent enriched categories and the enriched Rezk completion
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)
