Impredicative Encodings of (Higher) Inductive Types

Steve Awodey, Jonas Frey, Sam Speight

Type: Article

Publication Date: 2018-06-27

Citations: 18

DOI: https://doi.org/10.1145/3209108.3209130

Locations

arXiv (Cornell University) - View - PDF

Similar Works

Action	Title	Year	Authors
+	Impredicative Encodings of (Higher) Inductive Types	2018	Steve Awodey Jonas Frey Sam Speight
+	Computational Higher Type Theory IV: Inductive Types	2018	Evan Cavallo Robert Harper
+	Functions out of Higher Truncations	2015	Paolo Capriotti Nicolai Kraus Andrea Vezzosi
+	Functions out of Higher Truncations	2015	Paolo Capriotti Nicolai Kraus Andrea Vezzosi
+	Two tricks to trivialize higher-indexed families	2023	Tesla Zhang
+	Induction and subduction of type-adapted representations	1982	P. Kasperkovitz
+	Type-Reduction	2017	Jerry M. Mendel
+	Truncation levels in homotopy type theory	2015	Nicolai Kraus
+	Functions out of Higher Truncations	2015	Paolo Capriotti Nicolai Kraus Andrea Vezzosi
+	Construction of the Circle in UniMath	2019	Marc Bezem Ulrik Buchholtz Daniel R. Grayson Michael Shulman
+	Construction of the Circle in UniMath	2019	Marc Bezem Ulrik Buchholtz Daniel R. Grayson Michael Shulman
+	Signatures and Induction Principles for Higher Inductive-Inductive Types	2019	Ambrus Kaposi András Kovács
+	Higher inductive types in Homotopy Type Theory: applications and theory	2016	Fredrik Nordvall Forsberg
+ PDF Chat	Path Spaces of Higher Inductive Types in Homotopy Type Theory	2019	Nicolai Kraus Jakob von Raumer
+	Constructing the Propositional Truncation using Non-recursive HITs	2015	Floris van Doorn
+	Constructing the Propositional Truncation using Non-recursive HITs	2015	Floris van Doorn
+ PDF Chat	Constructing the propositional truncation using non-recursive HITs	2016	Floris van Doorn
+	Path Spaces of Higher Inductive Types in Homotopy Type Theory	2019	Nicolai Kraus Jakob von Raumer
+	Path Spaces of Higher Inductive Types in Homotopy Type Theory	2019	Nicolai Kraus Jakob von Raumer
+	Higher Inductive Types as Homotopy-Initial Algebras	2014	Kristina Sojakova

Works That Cite This (13)

Action	Title	Year	Authors
+ PDF Chat	Groupoidal realizability for intensional type theory	2024	Samuel L. Speight
+	Cubical Assemblies, a Univalent and Impredicative Universe and a Failure of Propositional Resizing	2018	Taichi Uemura
+	Impredicative Encodings of (Higher) Inductive Types	2018	Steve Awodey Jonas Frey Sam Speight
+	Some Remarks About Dependent Type Theory	2023	Thierry Coquand
+ PDF Chat	Constructing Higher Inductive Types as Groupoid Quotients	2021	Niccolò Veltri Niels van der Weide
+ PDF Chat	Constructing quotient inductive-inductive types	2019	Ambrus Kaposi András Kovács Thorsten Altenkirch
+	Cubical Assemblies and Independence of the Propositional Resizing Axiom.	2018	Taichi Uemura
+	A Note on Generalized Algebraic Theories and Categories with Families	2020	Marc Bezem Thierry Coquand Peter Dybjer Martı́n Hötzel Escardó
+	The Yoneda Reduction of Polymorphic Types (Extended Version)	2019	Paolo Pistone Luca Tranchini
+	Parametricity via Cohesion	2024	C. B. Aberlé

Works Cited by This (13)

Action	Title	Year	Authors
+ PDF Chat	Towards a theory of type structure	1974	John Reynolds
+	Extensional concepts in intensional type theory	1995	Martin Hofmann
+ PDF Chat	Wellfounded Trees and Dependent Polynomial Functors	2004	Nicola Gambino Martin Hyland
+	Une théorie combinatoire des séries formelles	1981	André Joyal
+ PDF Chat	Higher Inductive Types as Homotopy-Initial Algebras	2014	Kristina Sojakova
+ PDF Chat	Univalent categories and the Rezk completion	2015	Benedikt Ahrens Krzysztof Kapulkin Michael Shulman
+ PDF Chat	Calculating the Fundamental Group of the Circle in Homotopy Type Theory	2013	Daniel R. Licata Michael Shulman
+	A small complete category	1988	J. M. E. Hyland
+ PDF Chat	Type theories, toposes and constructive set theory: predicative aspects of AST	2002	Ieke Moerdijk Erik Palmgren
+	Impredicative Encodings of (Higher) Inductive Types	2018	Steve Awodey Jonas Frey Sam Speight