The construction of set-truncated higher inductive types (Q2133178): Difference between revisions

@@ Property / describes a project that uses @@
+UniMath
@@ Property / describes a project that uses: UniMath / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+cubicaltt
@@ Property / describes a project that uses: cubicaltt / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1016/j.entcs.2019.09.014
+Normal rank
@@ Property / OpenAlex ID @@
+W2994973104
@@ Property / OpenAlex ID: W2994973104 / rank @@
+Normal rank
@@ Property / Wikidata QID @@
+Q113317349
@@ Property / Wikidata QID: Q113317349 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5089004
@@ Property / cites work: Q5089004 / rank @@
+Normal rank
@@ Property / cites work @@
+Univalent categories and the Rezk completion
@@ Property / cites work: Univalent categories and the Rezk completion / rank @@
+Normal rank
@@ Property / cites work @@
+Displayed Categories
@@ Property / cites work: Displayed Categories / rank @@
+Normal rank
@@ Property / cites work @@
+Quotient inductive-inductive types
@@ Property / cites work: Quotient inductive-inductive types / rank @@
+Normal rank
@@ Property / cites work @@
+Partiality, Revisited
@@ Property / cites work: Partiality, Revisited / rank @@
+Normal rank
@@ Property / cites work @@
+Type theory in type theory using quotient inductive types
+Normal rank
@@ Property / cites work @@
+Q5371043
@@ Property / cites work: Q5371043 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4649535
@@ Property / cites work: Q4649535 / rank @@
+Normal rank
@@ Property / cites work @@
+Computational higher-dimensional type theory
@@ Property / cites work: Computational higher-dimensional type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Homotopical patch theory
@@ Property / cites work: Homotopical patch theory / rank @@
+Normal rank
@@ Property / cites work @@
+Inductive Types in Homotopy Type Theory
@@ Property / cites work: Inductive Types in Homotopy Type Theory / rank @@
+Normal rank
@@ Property / cites work @@
+Q2968413
@@ Property / cites work: Q2968413 / rank @@
+Normal rank
@@ Property / cites work @@
+Quotienting the delay monad by weak bisimilarity
@@ Property / cites work: Quotienting the delay monad by weak bisimilarity / rank @@
+Normal rank
@@ Property / cites work @@
+Cubical Type Theory: a constructive interpretation of the univalence axiom
+Normal rank
@@ Property / cites work @@
+On Higher Inductive Types in Cubical Type Theory
@@ Property / cites work: On Higher Inductive Types in Cubical Type Theory / rank @@
+Normal rank
@@ Property / cites work @@
+Inductive families
@@ Property / cites work: Inductive families / rank @@
+Normal rank
@@ Property / cites work @@
+Finitary higher inductive types in the groupoid model
+Normal rank
@@ Property / cites work @@
+A Type-Theoretical Definition of Weak {\omega}-Categories
+Normal rank
@@ Property / cites work @@
+Structural induction and coinduction in a fibrational setting
+Normal rank
@@ Property / cites work @@
+Wild omega-Categories for the Homotopy Hypothesis in Type Theory
+Normal rank
@@ Property / cites work @@
+A Syntax for Higher Inductive-Inductive Types
@@ Property / cites work: A Syntax for Higher Inductive-Inductive Types / rank @@
+Normal rank
@@ Property / cites work @@
+The simplicial model of univalent foundations (after Voevodsky)
+Normal rank
@@ Property / cites work @@
+Constructions with Non-Recursive Higher Inductive Types
+Normal rank
@@ Property / cites work @@
+Eilenberg-MacLane spaces in homotopy type theory
@@ Property / cites work: Eilenberg-MacLane spaces in homotopy type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Calculating the Fundamental Group of the Circle in Homotopy Type Theory
+Normal rank
@@ Property / cites work @@
+Weak ω-Categories from Intensional Type Theory
@@ Property / cites work: Weak ω-Categories from Intensional Type Theory / rank @@
+Normal rank
@@ Property / cites work @@
+Semantics of higher inductive types
@@ Property / cites work: Semantics of higher inductive types / rank @@
+Normal rank
@@ Property / cites work @@
+Q5639839
@@ Property / cites work: Q5639839 / rank @@
+Normal rank
@@ Property / cites work @@
+The real projective spaces in homotopy type theory
+Normal rank
@@ Property / cites work @@
+Sets in homotopy type theory
@@ Property / cites work: Sets in homotopy type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Higher Inductive Types as Homotopy-Initial Algebras
+Normal rank
@@ Property / cites work @@
+The formal theory of monads
@@ Property / cites work: The formal theory of monads / rank @@
+Normal rank
@@ Property / cites work @@
+Homotopy Type Theory: Univalent Foundations of Mathematics
+Normal rank
@@ Property / cites work @@
+Types are weak <i>ω</i> -groupoids
@@ Property / cites work: Types are weak <i>ω</i> -groupoids / rank @@
+Normal rank