The Marriage of Univalence and Parametricity

Nicolas Tabareau, Éric Tanter, Matthieu Sozeau

Type: Preprint

Publication Date: 2019-09-11

Citations: 3

Locations

arXiv (Cornell University) - View

Similar Works

Action	Title	Year	Authors
+	The Marriage of Univalence and Parametricity	2019	Nicolas Tabareau Éric Tanter Matthieu Sozeau
+ PDF Chat	The Marriage of Univalence and Parametricity	2021	Nicolas Tabareau Éric Tanter Matthieu Sozeau
+ PDF Chat	Trocq: Proof Transfer for Free, With or Without Univalence	2024	Cyril Cohen Enzo Crance Assia Mahboubi
+	Type Classes for Mathematics in Type Theory	2011	Bas Spitters Eelis van der Weegen
+	Type Classes for Mathematics in Type Theory	2011	Bas Spitters Eelis van der Weegen
+ PDF Chat	Type classes for mathematics in type theory	2011	Bas Spitters Eelis van der Weegen
+ PDF Chat	Internal Parametricity for Cubical Type Theory	2021	Evan Cavallo Robert Harper
+	Internal Parametricity for Cubical Type Theory	2020	Evan Cavallo Robert Harper
+	Internal Parametricity for Cubical Type Theory	2020	Evan Cavallo Robert Harper
+	Parametricity in an Impredicative Sort	2012	Chantal Keller Marc Lasson
+	Parametric Cubical Type Theory	2019	Evan Cavallo Robert Harper
+	Shallow Embedding of Type Theory is Morally Correct	2019	Ambrus Kaposi András Kovács Nicolai Kraus
+	Shallow Embedding of Type Theory is Morally Correct	2019	Ambrus Kaposi András Kovács Nicolai Kraus
+ PDF Chat	A weak HOAS approach to the POPLmark Challenge	2013	Alberto Ciaffaglione Ivan Scagnetto
+ PDF Chat	Is sized typing for Coq practical?	2023	Jonathan Chan YUFENG LI William J. Bowman
+	Is Sized Typing for Coq Practical?	2019	Jonathan Chan Yu-Feng Li William J. Bowman
+	Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant	2015	Théo Zimmermann Hugo Herbelin
+ PDF Chat	The Refined Calculus of Inductive Construction: Parametricity and Abstraction	2012	Chantal Keller Marc Lasson
+	The Refined Calculus of Inductive Construction: Parametricity and Abstraction	2012	Chantal Keller Marc Lasson
+	Towards Proof Repair in Cubical Agda	2023	Cosmo Viola Max Fan Talia Ringer

Works That Cite This (3)

Action	Title	Year	Authors
+ PDF Chat	Proof repair across type equivalences	2021	Talia Ringer RanDair Porter Nathaniel Yazdani John Leo Dan Grossman
+	Internalizing Representation Independence with Univalence	2020	Carlo Angiuli Evan Cavallo Anders Mörtberg Max Zeuner
+	Functional Extensionality for Refinement Types.	2021	Niki Vazou Michael Greenberg

Works Cited by This (11)

Action	Title	Year	Authors
+	Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant	2015	Théo Zimmermann Hugo Herbelin
+	Homotopy Type Theory: Univalent Foundations of Mathematics	2013	Peter Aczel Benedikt Ahrens Thorsten Altenkirch Steve Awodey Bruno Barras Andrej Bauer Yves Bertot Marc Bezem Thierry Coquand Eric Finster
+ PDF Chat	Transporting functions across ornaments	2014	PIERRE-ÉVARISTE DAGAND Conor McBride
+	The HoTT library: a formalization of homotopy type theory in Coq	2016	Andrej Bauer Jason Gross Peter LeFanu Lumsdaine Michael Shulman Matthieu Sozeau Bas Spitters
+ PDF Chat	Cubical Type Theory: a constructive interpretation of the univalence axiom	2015	Cyril Cohen Thierry Coquand Simon Huber Anders Mörtberg
+	The equivalence axiom and univalent models of type theory. (Talk at CMU on February 4, 2010)	2014	Vladimir Voevodsky
+	Revisiting Parametricity: Inductives and Uniformity of Propositions	2017	Abhishek Anand Greg Morrisett
+	Towards a Cubical Type Theory without an Interval.	2015	Thorsten Altenkirch Ambrus Kaposi
+	Homotopical inverse diagrams in categories with attributes	2018	Chris Kapulkin Peter LeFanu Lumsdaine
+	Internal Parametricity for Cubical Type Theory	2020	Evan Cavallo Robert Harper