pith. sign in

arxiv: 2402.12169 · v4 · submitted 2024-02-19 · 💻 cs.LO

Automating Boundary Filling in Cubical Type Theories

Maximilian Dor\'e , Evan Cavallo , Anders M\"ortberg This is my paper

Pith reviewed 2026-05-24 04:03 UTC · model grok-4.3

classification 💻 cs.LO
keywords cubical type theorycontortion solvingKan solvingboundary fillingposet mapsconstraint satisfactionproof automationhomotopy type theory
0
0 comments X

The pith

Reformulating contortions as poset maps yields solvers for boundary filling in cubical type theories.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper isolates two automation problems in cubical type theory: contorting a single cube to match a prescribed boundary and the broader Kan solving task of finding pastings of multiple cubes. It shows that contortions in the Dedekind and De Morgan theories can be solved once they are recast as maps between posets, while constraint satisfaction programming handles Kan problems uniformly regardless of the chosen contortion theory. These routines target the higher-dimensional equations that appear when working with higher inductive types and univalence inside proof assistants. A sympathetic reader would care because the combinatorics grow rapidly with dimension and manual solutions become impractical. The algorithms are implemented in an experimental Haskell solver and demonstrated on the Eckmann-Hilton theorem together with a set of benchmarks.

Core claim

By reformulating contortions in terms of poset maps, the paper supplies a solver for the contortion problem in the Dedekind and De Morgan contortion theories; it solves the more general Kan problems by constraint satisfaction programming that works independently of the underlying contortion theory, all inside a simplified cubical language designed to study these two automation tasks.

What carries the argument

The reformulation of contortions as poset maps, which converts boundary-fitting into a search for order-preserving maps, together with constraint satisfaction programming to assemble solutions from multiple cubes.

If this is right

  • Many routine higher-dimensional equations between algebraic expressions become automatically solvable.
  • Proofs such as the Eckmann-Hilton theorem can be completed with substantially less manual cube construction.
  • The same Kan solver applies across Dedekind, De Morgan, and other contortion theories without modification.
  • Users of cubical type theory gain a uniform method for discharging boundary-filling obligations.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The poset-map view may transfer to automation problems in related higher-dimensional combinatorial settings.
  • Embedding the solver inside an existing proof assistant could reduce the size of formal developments that rely on cubical features.
  • Further search heuristics could be added to handle cases that currently exceed the practical reach of the current constraint solver.

Load-bearing premise

Heuristics built on these techniques will succeed on the practical examples that arise in actual cubical type theory developments despite the general undecidability of the problems.

What would settle it

A benchmark suite of representative higher-dimensional goals drawn from cubical type theory libraries on which the solver either times out or returns no solution even though a filling exists.

Figures

Figures reproduced from arXiv: 2402.12169 by Anders M\"ortberg, Evan Cavallo, Maximilian Dor\'e.

Figure 1
Figure 1. Figure 1: A cubical Eckmann-Hilton argument in four steps. In cubical type theory, we can construct such an interior by starting from some 3-cube we know can be filled, then deforming its boundary via certain basic operations until it has the desired form. It can be more intuitive to work backwards: deform the “goal” boundary until we reach a boundary we can fill [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
read the original abstract

When working in a proof assistant, automation is key to discharging routine proof goals such as equations between algebraic expressions. Homotopy type theory allows the user to reason about higher structures, such as topological spaces, using higher inductive types (HITs) and univalence. Cubical type theory provides computational support for HITs and univalence. A difficulty when working in cubical type theory is dealing with the complex combinatorics of higher structures, an infinite-dimensional generalisation of equational reasoning. To solve these higher-dimensional equations consists in constructing cubes with specified boundaries. We develop a simplified cubical language in which we isolate and study two automation problems: contortion solving, where we attempt to "contort" a cube to fit a given boundary, and the more general Kan solving, where we search for solutions that involve pasting multiple cubes together. Both problems are difficult in the general case-Kan solving is even undecidable-so we focus on heuristics that perform well on practical examples. Our language encompasses different variations of cubical type theory which differ in their "contortion theory", i.e., the class of contortions they support. We provide a solver for the contortion problem for the most complex contortion theories currently being researched, the Dedekind and De Morgan contortions, by utilizing a reformulation of contortions in terms of poset maps. We solve Kan problems using constraint satisfaction programming, which is applicable independently of the underlying contortion theory. We have implemented our algorithms in an experimental Haskell solver that can be used to automatically solve many goals a user of cubical type theory might face. We illustrate this with a case study establishing the Eckmann-Hilton theorem using our solver, as well as various benchmarks.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The paper develops a simplified cubical language isolating two automation problems: contortion solving (fitting a cube to a boundary) and the more general Kan solving (pasting multiple cubes). It reformulates contortions as poset maps to solve the problem for Dedekind and De Morgan contortion theories, encodes Kan problems via constraint satisfaction programming (independent of the contortion theory), implements the solvers in an experimental Haskell tool, and demonstrates utility via the Eckmann-Hilton theorem case study plus benchmarks. Both problems are noted as generally difficult or undecidable, with focus on practical heuristics.

Significance. If the solvers are correct as described, the work supplies practical automation for routine higher-dimensional goals in cubical type theory, a recognized bottleneck in proof assistants supporting HITs and univalence. Strengths include the explicit separation of concerns between contortion and Kan solving, the theory-independent CSP encoding, the shipped Haskell implementation, and the concrete Eckmann-Hilton case study, all of which support reproducibility and applicability.

minor comments (3)
  1. [Abstract] Abstract: the claim that the CSP approach 'is applicable independently of the underlying contortion theory' is central but would benefit from an explicit statement of the interface between the CSP solver and the contortion theory (e.g., which operations are delegated to the poset-map solver).
  2. [Implementation and benchmarks] The paper states that heuristics 'perform well on practical examples' after acknowledging general undecidability; a table or subsection quantifying success rates, timeout behavior, or comparison to a baseline solver on the reported benchmarks would strengthen this empirical claim.
  3. [Case study] The Eckmann-Hilton case study is presented as evidence of utility; clarifying which specific contortion and Kan goals were discharged automatically versus those requiring manual intervention would make the contribution more precise.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary, significance assessment, and recommendation of minor revision. The report correctly identifies the core contributions: isolating contortion and Kan problems, the poset-map reformulation for Dedekind/De Morgan theories, the theory-independent CSP encoding for Kan problems, the Haskell implementation, and the Eckmann-Hilton case study. No specific major comments were raised, so our response focuses on confirming the overall evaluation and noting that we will perform the minor revision as recommended.

Circularity Check

0 steps flagged

No significant circularity; implementation uses independent standard techniques

full rationale

The paper's central contributions are an algorithmic reformulation of contortions as poset maps (drawing on standard order theory) and a CSP encoding for Kan problems (standard constraint programming), both presented as applicable independently of the specific contortion theory. The text explicitly notes undecidability in the general case and restricts to heuristics, with support from an external Haskell implementation and Eckmann-Hilton case study. No self-definitional reductions, fitted inputs renamed as predictions, or load-bearing self-citations appear in the provided abstract or description; the derivation chain remains self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

The work rests on standard mathematical concepts from order theory and constraint programming with no new free parameters, axioms beyond ordinary mathematics, or invented entities.

pith-pipeline@v0.9.0 · 5849 in / 1076 out tokens · 30628 ms · 2026-05-24T04:03:02.610565+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

47 extracted references · 47 canonical work pages · 2 internal anchors

  1. [1]

    Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Robert Harper, Kuen-Bang Hou (Favonia), and Daniel R. Licata. Syntax and models of Cartesian cubical type theory . Mathematical Structures in Computer Science , 31(4):424--468, 2021. https://doi.org/10.1017/S0960129521000347 doi:10.1017/S0960129521000347

    work page doi:10.1017/s0960129521000347 2021

  2. [2]

    Polygraphs: From rewriting to higher categories

    Dimitri Ara, Albert Burroni, Yves Guiraud, Philippe Malbos, François Métayer, and Samuel Mimram. Polygraphs: From rewriting to higher categories. Submitted, 2023. https://arxiv.org/abs/2312.00429 arXiv:2312.00429

    work page arXiv 2023

  3. [3]

    The equivariant model structure on cartesian cubical sets

    Steve Awodey, Evan Cavallo, Thierry Coquand, Emily Riehl, and Christian Sattler. The equivariant model structure on cartesian cubical sets, 2024. https://arxiv.org/abs/2406.18497 arXiv:2406.18497

    work page internal anchor Pith review Pith/arXiv arXiv 2024

  4. [4]

    Explicit substitutions

    Mart\' i n Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacque L\' e vy. Explicit substitutions. Journal of Functional Programming , 1(4):375--416, 1991. https://doi.org/10.1017/S0956796800000186 doi:10.1017/S0956796800000186

    work page doi:10.1017/s0956796800000186 1991

  5. [5]

    Cartesian cubical computational type theory: Constructive reasoning with paths and equalities

    Carlo Angiuli, Kuen-Bang Hou (Favonia), and Robert Harper. Cartesian cubical computational type theory: Constructive reasoning with paths and equalities. In 27th EACSL Annual Conference on Computer Science Logic, CSL 2018, September 4-7, 2018, Birmingham, UK , pages 6:1--6:17, 2018. https://doi.org/10.4230/LIPIcs.CSL.2018.6 doi:10.4230/LIPIcs.CSL.2018.6

    work page doi:10.4230/lipics.csl.2018.6 2018

  6. [6]

    Cartesian cubical model categories, 2023

    Steve Awodey. Cartesian cubical model categories, 2023. https://arxiv.org/abs/2305.00893 arXiv:2305.00893

    work page arXiv 2023

  7. [7]

    Ronald Brown and Philip J. Higgins. On the algebra of cubes. Journal of Pure and Applied Algebra , 21(3):233--260, 1981. https://doi.org/10.1016/0022-4049(81)90018-9 doi:10.1016/0022-4049(81)90018-9

    work page doi:10.1016/0022-4049(81)90018-9 1981

  8. [8]

    Rings of sets

    Garrett Birkhoff. Rings of sets. Duke Mathematical Journal , 3(3):443--454, 1937. https://doi.org/10.1215/S0012-7094-37-00334-X doi:10.1215/S0012-7094-37-00334-X

    work page doi:10.1215/s0012-7094-37-00334-x 1937

  9. [9]

    Higher eckmann-hilton arguments in type theory, 2025

    Thibaut Benjamin, Ioannis Markakis, Wilfred Offord, Chiara Sarti, and Jamie Vicary. Higher eckmann-hilton arguments in type theory, 2025. URL: https://arxiv.org/abs/2501.16465, https://arxiv.org/abs/2501.16465 arXiv:2501.16465

    work page arXiv 2025

  10. [10]

    Naturality for higher-dimensional path types

    Thibaut Benjamin, Ioannis Markakis, Wilfred Offord, Chiara Sarti, and Jamie Vicary. Naturality for higher-dimensional path types . In Proceedings of the 40th Annual ACM/IEEE Symposium on Logic in Computer Science , LICS '25. ACM, 2025

    work page 2025

  11. [11]

    On the homotopy groups of spheres in homotopy type theory

    Guillaume Brunerie. On the homotopy groups of spheres in homotopy type theory . PhD thesis, Universit\'e de Nice Sophia Antipolis, 2016

    work page 2016

  12. [12]

    Computer-generated proofs for the monoidal structure of the smash product

    Guillaume Brunerie. Computer-generated proofs for the monoidal structure of the smash product. Homotopy Type Theory Electronic Seminar Talks, November 2018. URL: https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html

    work page 2018

  13. [13]

    Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom

    Cyril Cohen, Thierry Coquand, Simon Huber, and Anders M \"o rtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom . In Tarmo Uustalu, editor, 21st International Conference on Types for Proofs and Programs (TYPES 2015) , volume 69 of LIPIcs , pages 5:1--5:34. Schloss Dagstuhl, 2018. https://doi.org/10.4230/LIPIcs.TYPES.2015.5 d...

    work page doi:10.4230/lipics.types.2015.5 2015

  14. [14]

    On Higher Inductive Types in Cubical Type Theory

    Thierry Coquand, Simon Huber, and Anders M\" o rtberg. On Higher Inductive Types in Cubical Type Theory . In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science , LICS '18, pages 255--264. ACM, 2018. https://doi.org/10.1145/3209108.3209197 doi:10.1145/3209108.3209197

    work page doi:10.1145/3209108.3209197 2018

  15. [15]

    Donald J. Collins. A simple presentation of a group with unsolvable word problem. Illinois Journal of Mathematics , 30(2):230--234, 1986. https://doi.org/10.1215/ijm/1256044631 doi:10.1215/ijm/1256044631

    work page doi:10.1215/ijm/1256044631 1986

  16. [16]

    Relative elegance and cartesian cubes with one connection, 2023

    Evan Cavallo and Christian Sattler. Relative elegance and cartesian cubes with one connection, 2023. https://arxiv.org/abs/2211.14801 arXiv:2211.14801

    work page arXiv 2023

  17. [17]

    Daniel Christensen and Luis Scoccola

    J. Daniel Christensen and Luis Scoccola. The Hurewicz theorem in Homotopy Type Theory . Algebraic & Geometric Topology , 23:2107--2140, 2023

    work page 2023

  18. [18]

    Automating Boundary Filling in Cubical Agda

    Maximilian Dor\' e , Evan Cavallo, and Anders M\" o rtberg. Automating Boundary Filling in Cubical Agda . In Jakob Rehof, editor, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024) , volume 299 of Leibniz International Proceedings in Informatics (LIPIcs) , pages 22:1--22:18, Dagstuhl, Germany, 2024. Schloss Dagstuh...

    work page doi:10.4230/lipics.fscd.2024.22 2024

  19. [19]

    Associative n -categories

    Christoph Dorn. Associative n -categories . PhD thesis, University of Oxford, 2018

    work page 2018

  20. [20]

    Beno Eckmann and Peter J. Hilton. Group-like structures in general categories I : multiplications and comultiplications. Mathematische Annalen , 145:227--255, 1962

    work page 1962

  21. [21]

    A type-theoretical definition of weak -categories

    Eric Finster and Samuel Mimram. A type-theoretical definition of weak -categories. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) , pages 1--12, 2017. https://doi.org/10.1109/LICS.2017.8005124 doi:10.1109/LICS.2017.8005124

    work page doi:10.1109/lics.2017.8005124 2017

  22. [22]

    A type theory for strictly unital -categories

    Eric Finster, David Reutter, Jamie Vicary, and Alex Rice. A type theory for strictly unital -categories. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) , pages 1--12, 2022. https://doi.org/10.1145/3531130.3533363 doi:10.1145/3531130.3533363

    work page doi:10.1145/3531130.3533363 2022

  23. [23]

    Walker, and Elbert A

    Mai Gehrke, Carol L. Walker, and Elbert A. Walker. Normal forms and truth tables for fuzzy logics. Fuzzy Sets and Systems , 138(1):25--51, 2003. URL: https://www.sciencedirect.com/science/article/pii/S0165011402005663, https://doi.org/10.1016/S0165-0114(02)00566-3 doi:10.1016/S0165-0114(02)00566-3

    work page doi:10.1016/s0165-0114(02)00566-3 2003

  24. [24]

    A computation of D(9) using FPGA Supercomputing , 2023

    Lennart Van Hirtum, Patrick De Causmaecker, Jens Goemaere, Tobias Kenter, Heinrich Riebler, Michael Lass, and Christian Plessl. A computation of D(9) using FPGA Supercomputing , 2023. https://arxiv.org/abs/2304.03039 arXiv:2304.03039

    work page arXiv 2023

  25. [25]

    In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Com- puter Science

    Kuen-Bang Hou (Favonia) , Eric Finster, Daniel R. Licata, and Peter LeFanu Lumsdaine. A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory . In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science , LICS '16, pages 565--574. Association for Computing Machinery, 2016. https://doi.org/10.1145/2933575.2...

    work page doi:10.1145/2933575.2934545 2016

  26. [26]

    The Seifert-van Kampen Theorem in Homotopy Type Theory

    Kuen-Bang Hou (Favonia) and Michael Shulman. The Seifert-van Kampen Theorem in Homotopy Type Theory . In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016) , volume 62 of Leibniz International Proceedings in Informatics (LIPIcs) , pages 22:1--22:16, Dagstuhl, Germany, 2016. Schloss Dagstuhl--Le...

    work page doi:10.4230/lipics.csl.2016.22 2016

  27. [27]

    Stone Spaces , volume 3 of Cambridge Studies in Advanced Mathematics

    Peter Tennant Johnstone. Stone Spaces , volume 3 of Cambridge Studies in Advanced Mathematics . Cambridge University Press, 1986

    work page 1986

  28. [28]

    A computation of the ninth Dedekind Number , 2023

    Christian Jäkel. A computation of the ninth Dedekind Number , 2023. https://arxiv.org/abs/2304.00895 arXiv:2304.00895

    work page arXiv 2023

  29. [29]

    Daniel M. Kan. Abstract homotopy.\ I . Proceedings of the National Academy of Sciences of the United States of America , 41(12):1092--1096, 1955

    work page 1955

  30. [30]

    A language and a program for stating and solving combinatorial problems

    Jean-Louis Lauri \`e re. A language and a program for stating and solving combinatorial problems. Artificial Intelligence , 10(1):29--127, 1978. https://doi.org/10.1016/0004-3702(78)90029-2 doi:10.1016/0004-3702(78)90029-2

    work page doi:10.1016/0004-3702(78)90029-2 1978

  31. [31]

    Movsisyan and V.A

    Yu.M. Movsisyan and V.A. Aslanyan. A functional completeness theorem for de morgan functions. Discrete Applied Mathematics , 162:1--16, 2014. URL: https://www.sciencedirect.com/science/article/pii/S0166218X13003478, https://doi.org/10.1016/j.dam.2013.08.006 doi:10.1016/j.dam.2013.08.006

    work page doi:10.1016/j.dam.2013.08.006 2014

  32. [32]

    An intuitionistic theory of types: Predicative part

    Per Martin-L \"o f. An intuitionistic theory of types: Predicative part. In H.E. Rose and J.C. Shepherdson, editors, Logic Colloquium '73 , volume 80 of Studies in Logic and the Foundations of Mathematics , pages 73 -- 118. Elsevier, 1975. https://doi.org/10.1016/S0049-237X(08)71945-1 doi:10.1016/S0049-237X(08)71945-1

    work page doi:10.1016/s0049-237x(08)71945-1 1975

  33. [33]

    The Lean mathematical library

    Anders M\" o rtberg and Lo\" c Pujet. Cubical Synthetic Homotopy Theory . In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs , CPP 2020, pages 158--171, New York, NY, USA, 2020. Association for Computing Machinery. https://doi.org/10.1145/3372885.3373825 doi:10.1145/3372885.3373825

    work page doi:10.1145/3372885.3373825 2020

  34. [34]

    Constraint Programming in Haskell

    David Overton. Constraint Programming in Haskell . Melbourne Haskell Users Group, 2015. URL: https://de.slideshare.net/davidoverton/constraint-programming-in-haskell

    work page 2015

  35. [35]

    On the complexity of some equivalence problems for propositional calculi

    Steffen Reith. On the complexity of some equivalence problems for propositional calculi. In Branislav Rovan and Peter Vojt \'a s , editors, Mathematical Foundations of Computer Science 2003 , volume 2747 of Lecture Notes in Computer Science , pages 632--641. Springer Berlin Heidelberg, 2003. https://doi.org/10.1007/978-3-540-45138-9_57 doi:10.1007/978-3-5...

    work page doi:10.1007/978-3-540-45138-9_57 2003

  36. [36]

    Robert Rose and Daniel R. Licata. Complexity of Cubical Cofibration Logics I: coNP-Complete Examples . In Rasmus Ejlers M gelberg and Benno van den Berg, editors, 30th International Conference on Types for Proofs and Programs (TYPES 2024) , volume 336 of Leibniz International Proceedings in Informatics (LIPIcs) , pages 9:1--9:21, Dagstuhl, Germany, 2025. ...

    work page doi:10.4230/lipics.types.2024.9 2024

  37. [37]

    A type theory for synthetic -categories

    Emily Riehl and Michael Shulman. A type theory for synthetic -categories. Higher Structures , 1(1):116--193, 2017

    work page 2017

  38. [38]

    Kristina Sojakova and G. A. Kavvos. Syllepsis in Homotopy Type Theory . In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) . Association for Computing Machinery, 2022. https://doi.org/10.1145/3531130.3533347 doi:10.1145/3531130.3533347

    work page doi:10.1145/3531130.3533347 2022

  39. [39]

    A sequent calculus for opetopes

    C \'e dric Ho Thanh, Pierre-Louis Curien, and Samuel Mimram. A sequent calculus for opetopes. In Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) , pages 1--12, 2019. https://doi.org/10.1109/LICS.2019.8785667 doi:10.1109/LICS.2019.8785667

    work page doi:10.1109/lics.2019.8785667 2019

  40. [40]

    The proof assistant, 2018

    The RedPRL Development Team . The proof assistant, 2018. URL: https://github.com/RedPRL/redtt/

    work page 2018

  41. [41]

    The 1Lab , 2023

    The 1Lab Development Team . The 1Lab , 2023. URL: https://1lab.dev

    work page 2023

  42. [42]

    Cubical Agda Library , October 2023

    The Agda Community . Cubical Agda Library , October 2023. URL: https://github.com/agda/cubical

    work page 2023

  43. [43]

    Foundations of Constraint Satisfaction

    Edward Tsang. Foundations of Constraint Satisfaction . Academic Press, 1993. https://doi.org/10.1016/C2013-0-07627-X doi:10.1016/C2013-0-07627-X

    work page doi:10.1016/c2013-0-07627-x 1993

  44. [44]

    Homotopy Type Theory: Univalent Foundations of Mathematics

    The Univalent Foundations Program . Homotopy Type Theory: Univalent Foundations of Mathematics . Institute for Advanced Study, 2013

    work page 2013

  45. [45]

    On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory

    Floris van Doorn. On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory . PhD thesis, Carnegie Mellon University, May 2018. URL: https://arxiv.org/abs/1808.10690

    work page internal anchor Pith review Pith/arXiv arXiv 2018

  46. [46]

    Cubical A gda: a Dependently Typed Programming Language With Univalence and Higher Inductive Types

    Andrea Vezzosi, Anders M \"o rtberg, and Andreas Abel. Cubical A gda: a Dependently Typed Programming Language With Univalence and Higher Inductive Types . Proceedings of the ACM on Programming Languages , 3(ICFP):1--29, 2019. https://doi.org/10.1145/3341691 doi:10.1145/3341691

    work page doi:10.1145/3341691 2019

  47. [47]

    The equivalence axiom and univalent models of type theory, February 2010

    Vladimir Voevodsky. The equivalence axiom and univalent models of type theory, February 2010. Notes from a talk at Carnegie Mellon University, available at http://www.math.ias.edu/vladimir/files/CMU_talk.pdf

    work page 2010