Truncation levels in homotopy type theory

Similar Works

Action	Title	Year	Authors
+	The General Universal Property of the Propositional Truncation	2014	Nicolai Kraus
+	The General Universal Property of the Propositional Truncation	2014	Nicolai Kraus
+ PDF Chat	The category of iterative sets in homotopy type theory and univalent foundations	2024	Daniel Gratzer Håkon Robbestad Gylterud Anders Mörtberg Elisabeth Stenholm
+ PDF Chat	The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations	2024	Daniel Gratzer Håkon Robbestad Gylterud Anders Mörtberg Elisabeth Stenholm
+	The General Universal Property of the Propositional Truncation	2015	Nicolai Kraus
+	The General Universal Property of the Propositional Truncation	2014	Nicolai Kraus
+ PDF Chat	Homotopy Type Theory: A Synthetic Approach to Higher Equalities	2018	Michael Shulman
+	π n (S n ) in Homotopy Type Theory	2013	Daniel R. Licata Guillaume Brunerie
+	Univalent Higher Categories via Complete Semi-Segal Types	2017	Paolo Capriotti Nicolai Kraus
+ PDF Chat	Univalent higher categories via complete Semi-Segal types	2017	Paolo Capriotti Nicolai Kraus
+	A Primer on Homotopy Type Theory Part 1: The Formal Type Theory	2014	James Ladyman Stuart Presnell
+	Models of Type Theory with Strict Equality	2017	Paolo Capriotti
+ PDF Chat	Sets in homotopy type theory	2015	Egbert Rijke Bas Spitters
+	Univalent Higher Categories via Complete Semi-Segal Types	2017	Paolo Capriotti Nicolai Kraus
+	Partial Univalence in n-truncated Type Theory	2020	Christian Sattler Andrea Vezzosi
+	Homotopy type theory	2012	Egbert Rijke
+	Extending Homotopy Type Theory with Strict Equality	2016	Thorsten Altenkirch Paolo Capriotti Nicolai Kraus
+	Partial Univalence in n-truncated Type Theory	2020	Christian Sattler Andrea Vezzosi
+	Voevodsky’s Univalence Axiom in Homotopy Type Theory	2013	Steve Awodey Álvaro Pelayo Michael A. Warren
+	Higher Lenses	2021	Paolo Capriotti Nils Anders Danielsson Andrea Vezzosi

Works That Cite This (13)

Action	Title	Year	Authors
+ PDF Chat	Homotopical inverse diagrams in categories with attributes	2020	Krzysztof Kapulkin Peter LeFanu Lumsdaine
+ PDF Chat	A rewriting coherence theorem with applications in homotopy type theory	2022	Nicolai Kraus Jakob von Raumer
+	Internal $\infty$-Categorical Models of Dependent Type Theory: Towards 2LTT Eating HoTT	2020	Nicolai Kraus
+	Homotopical inverse diagrams in categories with attributes	2018	Chris Kapulkin Peter LeFanu Lumsdaine
+	Free Higher Groups in Homotopy Type Theory	2018	Nicolai Kraus Thorsten Altenkirch
+ PDF Chat	Idempotents in intensional type theory	2017	Michael Shulman
+ PDF Chat	Constructive sheaf models of type theory	2021	Thierry Coquand Fabian Ruch Christian Sattler
+ PDF Chat	Higher Homotopies in a Hierarchy of Univalent Universes	2015	Nicolai Kraus Christian Sattler
+	Two-Level Type Theory and Applications.	2017	Danil Annenkov Paolo Capriotti Nicolai Kraus
+	Space-Valued Diagrams, Type-Theoretically (Extended Abstract).	2017	Nicolai Kraus Christian Sattler

Works Cited by This (39)

Action	Title	Year	Authors
+	Grothendieck $\infty$-groupoids, and still another definition of $\infty$-categories	2010	Georges Maltsiniotis
+	On automorphism groups of some finite groups	2003	Guohua Qian
+	Univalence in Simplicial Sets	2012	Chris Kapulkin Peter LeFanu Lumsdaine Vladimir Voevodsky
+	Extensional concepts in intensional type theory	1995	Martin Hofmann
+	Concrete Categories in Homotopy Type Theory	2013	James Cranch
+ PDF Chat	The Local Universes Model: An Overlooked Coherence Construction for Dependent Type Theories	2015	Peter LeFanu Lumsdaine Michael A. Warren
+	On the complexities of polymorphic stream equation systems, isomorphism of finitary inductive types, and higher homotopies in univalent universes	2015	Christian Sattler
+	Δ-SETS I: HOMOTOPY THEORY	1971	C. P. Rourke Brian Sanderson
+ PDF Chat	Topological and Simplicial Models of Identity Types	2012	Benno van den Berg Richard Garner
+	A model of type theory in simplicial sets	2013	Thomas Streicher