Pith. sign in

REVIEW 1 major objections 5 minor 86 references

Extension Types for Free

T0 review · 1 major / 5 minor · reviewed 2026-08-01 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read In two-level type theory, extension types are definable rather than postulated, and the definition validates the full extension-type calculus and makes cubical gluing equivalent to univalence.

desk verdict A formally checked 2LTT framework that derives extension types rather than postulating them, with a genuinely new gluing–univalence equivalence cycle; the strictness claims are conditional on the clearly-stated T1–T2 axioms. read the letter →

arxiv 2607.27387 v1 pith:4YW5CL6R submitted 2026-07-29 cs.LO math.ATmath.CTmath.LO

Nicolai Kraus This is my paper · ORCID
classification cs.LOmath.ATmath.CTmath.LO MSC 03B1503F50
keywords extensiontypestwo-leveltypetheorycofibrationscubicalunivalenceGluepathintervalconservativity
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper aims to show that extension types—types of partially determined terms, like paths with fixed endpoints—are not a new postulate needing bespoke semantics. Working in two-level type theory, which layers a strict equality on top of homotopy type theory, the paper defines the extension type along a cofibration as the strict fiber of a restriction map. This one definition makes the entire known extension-type calculus hold strictly: introduction, elimination, β, η, and boundary rules, with relative function extensionality and the homotopy extension property as theorems rather than axioms. The framework then lets the paper prove that cubical gluing and univalence are equivalent notions: univalence yields contractible Glue data along every cofibration, and a weak Glue structure on a path interval forces univalence. A sympathetic reader should care because this unifies scattered extension-type constructions and gives a concrete route toward comparing cubical type theory with original homotopy type theory.

What carries the argument

The load-bearing object is the extension type defined as the strict fiber of the restriction map i*: Π_Ψ A → Π_Φ (A∘i) over a partial section a, taken with the outer strict equality =s. Because the cofibration i is defined to make restriction preserve (trivial) fibrations, this strict fiber is automatically fibrant, which is what turns the definition into a type former with the right homotopy content. On the application side, the path interval—an interval whose endpoint inclusion is a cofibration and which carries a natural line-to-identity operation—is the detector that lets a weak Glue structure recover univalence.

What would settle it

Construct or locate a model of two-level type theory that satisfies the chosen axioms except that the inner-to-outer conversion preserves Π and Σ only up to homotopy, and check whether the boundary rule for the naive strict-fiber extension type still holds; the paper's Theorem 3.2 predicts it fails without on-the-nose preservation. Separately, any model with a path interval and a weak Glue structure but a non-univalent universe would directly contradict the paper's Theorem 5.14.

Watch

Extended reading notes

Core claim

The central claim, on the paper's own terms: in two-level type theory, once a class of cofibrations is fixed, the extension type defined as the strict fiber of the restriction map over a partial section is all that extension types ever were. Every rule of the known extension-type calculus holds strictly for this definition, and the axioms that other presentations postulate—notably relative function extensionality—are provable. The same framework makes the various cubical formulations of gluing collapse into a single cycle of implications: univalence implies contractible Glue data for every cofibration, and contractible data implies Glue structures, which imply weak Glue structures, which imp

Load-bearing premise

The whole derivation leans on the conversion from the inner to the outer level preserving Π, Σ, and the unit type on the nose; if that preservation were only up to homotopy, the strict boundary equality f∘i =s a in the extension type would need coercions and the strict extension-type rules would not follow automatically.

Editorial extensions

If this is right

  • Every model of the base homotopy type theory automatically yields a model with extension types, since two-level type theory is conservative and its semantics extend the standard models.
  • The extension-type rules hold strictly, and principles that were axioms in earlier presentations—relative function extensionality, the homotopy extension property—are theorems here.
  • Univalence implies contractible Glue data along every cofibration, so Glue types no longer need to be assumed as primitive cubical structure.
  • A weak Glue structure, requiring only inner equalities at the boundary and mere maps, is strong enough to imply univalence on a path interval.
  • The paper's comparison of the internal theories HoTT + (int) and Cub shows that gluing and univalence are inter-derivable over a path interval, pointing toward the open conservativity question.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Restricting the outer face calculus to a decidable sub-universe of strict propositions (a dominance or cofibration classifier) should recover decidable boundary checking from this framework without disturbing the theorems; the paper names this parametrization as future work.
  • The equivalence cycle suggests that in any type theory with a strict boundary layer, adding interval-like cofibrations and extension types secretly adds univalence; the strength is not in the Glue former but in the strict boundary discipline.
  • A natural test extension: instantiate the framework with a non-cubical shape layer—simplicial or tope-theoretic—and check which structural equivalences survive when the cofibration class is not meet-closed; the paper's union-law caveat predicts failures there.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

1 major / 5 minor

Summary. The paper develops a framework in two-level type theory (2LTT) in which extension types are defined rather than postulated. For a cofibration i : Φ → Ψ, a fibrant family A over Ψ, and a partial section a, the extension type is defined as the strict fiber of the restriction map over a (Definition 3.1). From this definition the paper derives the Riehl–Shulman extension-type calculus: the rules hold strictly (Theorem 3.2), the structural equivalences RS 4.1–4.5 become strict isomorphisms (Theorems 3.4–3.8), relative function extensionality becomes a theorem (Theorem 3.11), and realignment, extension extensionality, and the homotopy extension property follow (Corollary 3.12, Theorems 3.13–3.15). The paper then studies CCHM-style Glue, introduces several formulations (literal rules on sections, Glue structures, contractible Glue data, weak Glue structures), and proves that for a path interval univalence is equivalent to gluing in these senses (Theorem 5.15). The final section sketches a program, via 2LTT conservativity, toward the conjecture that cubical type theories are conservative over book HoTT. All results in Sections 2–5 are claimed to be formalized in Agda using the --two-level flag and Uskuplu's 2LTT library.

Significance. If correct, the paper gives a clean unification of the various extension-type notions in the literature and shows that a substantial portion of the Riehl–Shulman calculus is automatic once a cofibration class is fixed. The gluing–univalence equivalence is strong and reverses the usual Glue-to-univalence direction, giving a new internal characterization of univalence. A major strength is the machine-checked Agda formalization of the main body, including the representation-level fibrant-match statements. The main caveat—already disclosed by the author—is that the strictness of the extension-type calculus depends on the on-the-nose conversion axioms (T1)–(T2) of 2LTT; if conversion only preserved Π, Σ, and Unit up to homotopy, the strict boundary equalities and strict rules would degrade to propositional versions. Section 6 is explicitly a route toward the conservativity conjecture and is not formalized; it should not be read as a proof of that conjecture.

major comments (1)
  1. [§4.2, Lemma 4.2(2)] The proof asserts that from Θ being an equivalence one obtains glue(t,a) with strict boundary glue(t,a) ∘ i =s t. An element of the homotopy fiber of Θ over (t,a) only supplies an inner equality b∘i = t along with an equality of the unglue section; it does not, by itself, give the strict boundary. This matters because Corollary 5.5 and the advertised 'full constructor package up to homotopy, with term-bdry strict' depend on this point. The gap is probably repairable: when each unglue_γ is an equivalence, the type of b with b∘i =s t and unglue⊙b = a0 is contractible (unglue⊙(−) is an equivalence and the boundary condition is a strict proposition), and its center gives the required glue with strict term-bdry. Please spell this out, or explicitly refer to the formalized lemma Extension.GlueConstructorPackage for this precise step.
minor comments (5)
  1. [§2.1 / Abstract] The abstract says that 'the only genuine assumptions are which maps count as cofibrations.' This is too strong: the strictness of the entire development also assumes the on-the-nose conversion axioms (T1)–(T2) of Annenkov et al. The assumptions are stated in §2.1, but the abstract and the introduction's freeness claim should be qualified so that the reader does not expect the strict extension-type rules to survive in a 2LTT where conversion preserves structure only up to homotopy.
  2. [§2.1 / §2.2] Cross-reference mismatch: §2.1 refers to 'Theorem 2.1 below', but the numbered statement in §2.2 is Lemma 2.2. Similarly, §5.3 refers to 'Theorem 5.9' where the text labels it Remark 5.9, and the introduction refers to 'Theorem 4.2' where the heading is 'Lemma 4.2'.
  3. [Definition 5.11] The phrase 'family of mere maps u' is potentially confusing: 'mere' is used in HoTT for propositional truncation, but here it seems to mean 'plain functions without an equivalence witness'. Please use unambiguous terminology.
  4. [Formalization] The Agda documentation reference [1] points to Agda v2.6.3, while the paper says the development type-checks with Agda 2.8.0. Please update the reference or note the discrepancy. A commit hash or version pin for the repository would also improve reproducibility.
  5. [Title / Abstract] In the full text, the title is rendered as 'Extension Types for F ree'; this appears to be a formatting artifact and should be fixed.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity; the extension-type rules are unfolded from the explicit 2LTT/cofibration setup, and the gluing–univalence cycle does not presuppose its target.

full rationale

The derivation chain is self-contained relative to the stated two-level type theory framework. Definition 3.1 defines the extension type as the strict fiber of the restriction map, and Theorem 3.2 simply unfolds that definition into the Riehl–Shulman rules; this is an honest definitional realization rather than a fitted input called a prediction. Theorem 3.11 (relative function extensionality) is the trivial-fibration half of the definition of cofibration, explicitly acknowledged in the text: the proof says it uses exactly that half of the cofibration property. This is a transparent unpacking of an explicit framework assumption, not a hidden circular step. The gluing/univalence cycle is also non-circular: Theorem 5.4 derives contractible Glue data from univalence via the pointwise contractibility of W and relative funext, while Theorem 5.14 derives univalence from a weak Glue structure plus the path-interval lineToId structure, using the independent retraction lemma of Licata/Escardó (Lemma 5.10); it constructs a section of idtoeqv rather than assuming one. The paper explicitly flags its main caveat in Section 2.1: conversion is assumed to preserve Π, Σ, and Unit on the nose, 'as in axioms (T1)–(T2) of Annenkov et al. [7], to avoid coercions.' This is a stated framework hypothesis, not an internal circularity. Self-citations such as [7] supply the 2LTT axiomatics, cofibration facts, and conservativity; these are published external support with stated assumptions and are not an unverified uniqueness claim, and the paper's main body is additionally machine-checked in Agda. The score reflects a mild caveat about reliance on the imported 2LTT axioms, not a circular derivation.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The paper introduces no fitted parameters and no new postulates beyond the 2LTT framework. Its invented constructs are definitions (extension types as strict fibers, Glue structures, weak Glue structures, path intervals) rather than unexplained entities. The genuine assumptions are the 2LTT conversion axioms, the choice of a cofibration class, the cited semantic freeness of 2LTT, and the path-interval structure for the gluing–univalence equivalence.

assumptions (4)
  • domain assumption Two-level type theory: inner HoTT with intensional identity, outer strict MLTT with UIP and function extensionality, and a conversion preserving Π, Σ, Unit on the nose (axioms T1–T2 of [7]).
    Section 2.1 defines the framework. The strict boundary equalities used in extension types depend on the conversion preserving structure on the nose; this is assumed rather than proved in the paper.
  • domain assumption A chosen class of cofibrations in the outer level; extension types are relative to a cofibration, and the union law additionally requires meet-closure of the cofibration class and outer-level pushouts.
    Section 3 and Theorem 3.8. The paper itself identifies 'which maps count as cofibrations' as the only genuine assumption for the framework; arbitrary cofibrations need not be meet-closed.
  • domain assumption Semantic freeness and conservativity of 2LTT: every CwF-style model of HoTT yields a model of 2LTT, and 2LTT is conservative over its fibrant inner level.
    Cited to [7,20,42,15,72]. This underlies the claim that extension types come 'for free' semantically, but the model constructions and conservativity proofs are imported rather than reproved here.
  • domain assumption A path interval for the gluing–univalence cycle: a type I with 0,1, endpoint inclusion a cofibration, and a natural line-to-identity operation.
    Definition 5.6 and Theorem 5.15. The equivalence between gluing and univalence is conditional on this structure; not every model provides it automatically.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Extension Types for Free." pith.science (2026). https://pith.science/paper/4YW5CL6R

@misc{pith2026260727387,
  author       = {Pith},
  title        = {Pith review of: Extension Types for Free},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/4YW5CL6R}},
  note         = {Machine review of arXiv:2607.27387}
}
read the original abstract

Extension types are a concept in dependent type theory that has appeared in various contexts. The idea is to have types whose terms are partially determined, e.g. via a strict boundary condition. Standard examples are path types of cubical type theories (paths with fixed endpoints), Riehl and Shulman's name-giving extension types (terms fixed on subshapes), as well as the controlled-unfolding mechanism of cooltt and Agda (terms that are fixed if a condition is met). In each case, the type theory is equipped with a (meta-theoretic) face calculus, or shape layer, that governs their rules, and comes with intended semantics. We unify all these occurrences in a single framework where no new axioms or model constructions are needed, namely two-level type theory. This step, too, is free (semantically): the standard models of HoTT are automatically models of 2LTT, and the theory is conservative over HoTT. Extension types are definable, and the definition validates Riehl and Shulman's entire extension-type calculus: the rules hold strictly, and the postulated axioms, such as relative function extensionality, become theorems. In this way, every model of the base theory (HoTT) gives rise to a model of the same theory with extension types; the only genuine assumptions are which maps count as cofibrations. Conservativity makes the framework a tool for comparing type theories. We prove that cubical gluing, in a suitable formulation, is equivalent to univalence. On this basis, we suggest an approach toward the conjecture that cubical type theories are conservative over book HoTT, one of the central open problems of homotopy type theory. All results of the main body of the paper are auto-formalized in Agda --two-level, in a development that combines HoTT-internal arguments with reasoning that is external to HoTT.

Figures

Figures reproduced from arXiv: 2607.27387 by the authors.

Figure 1
Figure 1. The rules of extension types as presented in Riehl and Shulman [55, [PITH_FULL_IMAGE:figures/full_fig_p008_1.png] view at source ↗
Figure 2
Figure 2. CCHM gluing as presented in Cohen et al. [23, [PITH_FULL_IMAGE:figures/full_fig_p014_2.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

86 extracted references · 13 canonical work pages

  1. [1]

    Two-level type theory

    Agda documentation. Two-level type theory. https://agda.readthedocs.io/en/v2.6.3/ language/two-level.html, 2021

    2021

  2. [2]

    American Mathematical Society, 2025

    Benedikt Ahrens, Paige North, Michael Shulman, and Dimitris Tsementzis.The univa- lence principle, volume 305 ofMemoirs of the American Mathematical Society. American Mathematical Society, 2025

    2025

  3. [3]

    Extending homotopy type theory with strict equality

    Thorsten Altenkirch, Paolo Capriotti, and Nicolai Kraus. Extending homotopy type theory with strict equality. In Jean-Marc Talbot and Laurent Regnier, editors,25th EACSL Annual Conference on Computer Science Logic (CSL 2016), volume 62 ofLeibniz International Proceedings in Informatics (LIPIcs), pages 21:1–21:17. Schloss Dagstuhl — Leibniz-Zentrum f¨ ur I...

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

  4. [4]

    PhD thesis, Carnegie Mellon University, Pittsburgh, PA, USA, 2019

    Carlo Angiuli.Computational semantics of Cartesian cubical type theory. PhD thesis, Carnegie Mellon University, Pittsburgh, PA, USA, 2019

    2019

  5. [5]

    The RedPRL proof assistant (invited paper)

    Carlo Angiuli, Evan Cavallo, Kuen-Bang Hou (Favonia), Robert Harper, and Jonathan Sterling. The RedPRL proof assistant (invited paper). InProceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2018), volume 274 ofElectronic Proceedings in Theoretical Computer Science, pages 1–10, 2018. doi: 10.4...

    work page doi:10.4204/eptcs.274.1 2018

  6. [6]

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

    doi:10.1017/s0960129521000347 2021

  7. [7]

    Two-level type theory and applications.Mathematical Structures in Computer Science, 33(8):688–743, 2023

    Danil Annenkov, Paolo Capriotti, Nicolai Kraus, and Christian Sattler. Two-level type theory and applications.Mathematical Structures in Computer Science, 33(8):688–743, 2023. doi: 10.1017/s0960129523000130

    doi:10.1017/s0960129523000130 2023

  8. [8]

    The equivariant model structure on cartesian cubical sets.Advances in Mathematics, 495:110965,

    Steve Awodey, Evan Cavallo, Thierry Coquand, Emily Riehl, and Christian Sattler. The equivariant model structure on cartesian cubical sets.Advances in Mathematics, 495:110965,

Show all 86 references
  1. [9]

    sHoTT: formalisations for simplicial HoTT and synthetic ∞-categories, 2023

    Fredrik Bakke, Nikolai Kudasov, Jonathan Weinberger, Emily Riehl, Tashi Walde, and others. sHoTT: formalisations for simplicial HoTT and synthetic ∞-categories, 2023. URL https://github.com/rzk-lang/sHoTT. Rzk formalization library, started April 2023 as a fork of https://gith...

    2023

  2. [10]

    A model of type theory in cubical sets

    Marc Bezem, Thierry Coquand, and Simon Huber. A model of type theory in cubical sets. In Ralph Matthes and Aleksy Schubert, editors,19th International Conference on Types for Proofs and Programs (TYPES 2013), volume 26 ofLeibniz International Proceedings in Informatics (LIPIcs...

    2013

  3. [11]

    Coherence of strict equalities in dependent type theories

    Rafa¨ el Bocquet. Coherence of strict equalities in dependent type theories. arXiv:2010.14166, 2020

    2010 arXiv

  4. [12]

    External univalence for second-order generalized algebraic theories

    Rafa¨ el Bocquet. External univalence for second-order generalized algebraic theories. arXiv:2211.07487, 2022

    2022 arXiv

  5. [13]

    Towards coherence theorems for equational extensions of type theories

    Rafa¨ el Bocquet. Towards coherence theorems for equational extensions of type theories. arXiv:2304.10343, 2023

    2023 arXiv

  6. [14]

    Strict Rezk completions of models of HoTT and homotopy canonicity

    Rafa¨ el Bocquet. Strict Rezk completions of models of HoTT and homotopy canonicity. arXiv:2311.05849, 2023

    2023

  7. [15]

    PhD thesis, E¨ otv¨ os Lor´ and University, 2025

    Rafa¨ el Bocquet.Relative induction principles for second-order generalized algebraic the- ories. PhD thesis, E¨ otv¨ os Lor´ and University, 2025. Defended December 2025. https: //rafaelbocquet.gitlab.io/pdfs/thesis.pdf

    2025

  8. [16]

    A general cubical framework for coherence theorems

    Rafa¨ el Bocquet. A general cubical framework for coherence theorems. Abstract, Workshop on Homotopy Type Theory / Univalent Foundations (HoTT/UF 2026), Aarhus, Denmark,

    2026

  9. [17]

    For the metatheory of type theory, internal sconing is enough

    Rafa¨ el Bocquet, Ambrus Kaposi, and Christian Sattler. For the metatheory of type theory, internal sconing is enough. In8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), volume 260 ofLeibniz International Proceedings in Informatics (...

    2023

  10. [18]

    Homotopy type theory in Agda, fork by andrew swan, since 2012

    Guillaume Brunerie, Kuen-Bang Hou (Favonia), Evan Cavallo, Tim Baumann, Eric Fin- ster, Jesper Cockx, Christian Sattler, Chris Jeris, Michael Shulman, Andrew Swan, et al. Homotopy type theory in Agda, fork by andrew swan, since 2012. URL https: //github.com/awswan/HoTT-Agda

    2012

  11. [19]

    Available at https://hott-uf.github.io/2026/abstracts/HoTTUF_2026_paper_ 11.pdf

    2026

  12. [20]

    PhD thesis, University of Nottingham, 2017.https://eprints.nottingham.ac.uk/id/eprint/39382

    Paolo Capriotti.Models of type theory with strict equality. PhD thesis, University of Nottingham, 2017.https://eprints.nottingham.ac.uk/id/eprint/39382

    2017

  13. [21]

    Relative elegance and cartesian cubes with one connec- tion.Canadian Journal of Mathematics, 2025

    Evan Cavallo and Christian Sattler. Relative elegance and cartesian cubes with one connec- tion.Canadian Journal of Mathematics, 2025. doi: 10.4153/S0008414X25101466

    2025 doi

  14. [22]

    Eliminating reversals from cubical type theories

    Evan Cavallo and Christian Sattler. Eliminating reversals from cubical type theories. In 41st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2026), volume 380 ofLIPIcs, pages 27:1–27:27, 2026. doi: 10.4230/LIPIcs.LICS.2026.27

    2026 doi

  15. [23]

    Synthetic fibered ( ∞,1)-category theory.Higher Structures, 7(1):74–165, 2023

    Ulrik Buchholtz and Jonathan Weinberger. Synthetic fibered ( ∞,1)-category theory.Higher Structures, 7(1):74–165, 2023. doi: 10.21136/hs.2023.04

    2023 doi

  16. [24]

    Variations on cubical sets

    Thierry Coquand. Variations on cubical sets. Talk at Oxford Workshop on Homotopy Type Theory, 2014. URLhttps://www.cse.chalmers.se/ ~coquand/comp.pdf

    2014

  17. [25]

    Canonicity and homotopy canonicity for cubical type theory.Logical Methods in Computer Science, 18(1):28:1–28:35, 2022

    Thierry Coquand, Simon Huber, and Christian Sattler. Canonicity and homotopy canonicity for cubical type theory.Logical Methods in Computer Science, 18(1):28:1–28:35, 2022. doi: 10.46298/lmcs-18(1:28)2022

    2022 doi

  18. [26]

    Synthetic topology of data types and classical spaces.Electronic Notes in Theoretical Computer Science, 87:21–156, 2004

    Mart ´ ın H¨ otzel Escard´ o. Synthetic topology of data types and classical spaces.Electronic Notes in Theoretical Computer Science, 87:21–156, 2004. doi: 10.1016/j.entcs.2004.09.017

    2004 doi

  19. [27]

    Cubical type theory: A constructive interpretation of the univalence axiom

    Cyril Cohen, Thierry Coquand, Simon Huber, and Anders M¨ ortberg. Cubical type theory: A constructive interpretation of the univalence axiom. In Tarmo Uustalu, editor,21st 26 NICOLAI KRAUS International Conference on Types for Proofs and Programs (TYPES 2015), volume 69 of Lei...

    2015 doi

  20. [28]

    Towards a constructive simplicial model of univalent foundations.Journal of the London Mathematical Society, 105(2):1073–1109, 2022

    Nicola Gambino and Simon Henry. Towards a constructive simplicial model of univalent foundations.Journal of the London Mathematical Society, 105(2):1073–1109, 2022. doi: 10.1112/jlms.12532

    2022 doi

  21. [29]

    Directed univalence in simplicial homotopy type theory

    Daniel Gratzer, Jonathan Weinberger, and Ulrik Buchholtz. Directed univalence in simplicial homotopy type theory. arXiv:2407.09146, 2024

    2024

  22. [30]

    Controlling unfolding in type theory.Mathematical Structures in Computer Science, 35:e38,

    Daniel Gratzer, Jonathan Sterling, Carlo Angiuli, Thierry Coquand, and Lars Birkedal. Controlling unfolding in type theory.Mathematical Structures in Computer Science, 35:e38,

  23. [31]

    Any retraction of an identity type is an equivalence

    Mart ´ ın H¨ otzel Escard´ o. Any retraction of an identity type is an equivalence. Comment of 3 December on issue 718,Generalize 7.2.2 and simplify encode-decode, of the HoTT book repos- itory, 2014.https://github.com/HoTT/book/issues/718#issuecomment-65378867

    2014

  24. [32]

    The ∞-category of ∞-categories in simplicial type theory

    Daniel Gratzer, Jonathan Weinberger, and Ulrik Buchholtz. The ∞-category of ∞-categories in simplicial type theory. In Claudia Faggian and Joost-Pieter Katoen, editors,41st Annual Symposium on Logic in Computer Science (LICS 2026), volume 380 ofLeibniz International Proceeding...

    2026 doi

  25. [33]

    Robert Harper, Furio Honsell, and Gordon D. Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143–184, 1993. ISSN 0004-5411. doi: 10.1145/138027.138060. URLhttps://doi.org/10.1145/138027.138060

    1993

  26. [34]

    Conservativity of equality reflection over intensional type theory

    Martin Hofmann. Conservativity of equality reflection over intensional type theory. InTypes for Proofs and Programs (TYPES 1995), volume 1158 ofLecture Notes in Computer Science, pages 153–164. Springer, 1996. doi: 10.1007/3-540-61780-9 68

    1995 doi

  27. [35]

    Morita equivalences between algebraic dependent type theories

    Valery Isaev. Morita equivalences between algebraic dependent type theories. arXiv:1804.05045, 2018

    2018 arXiv

  28. [36]

    The Yoneda embedding in simplicial type theory

    Daniel Gratzer, Jonathan Weinberger, and Ulrik Buchholtz. The Yoneda embedding in simplicial type theory. In2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 127–142. IEEE, 2025. doi: 10.1109/LICS65433.2025.00017

    2025

  29. [37]

    Type theory in type theory using a strictified syntax

    Ambrus Kaposi and Lo ¨ ıc Pujet. Type theory in type theory using a strictified syntax. Proceedings of the ACM on Programming Languages, 9(ICFP):855–885, 2025. doi: 10.1145/ 3747535

    2025

  30. [38]

    Homotopy canonicity of homotopy type theory

    Chris Kapulkin and Christian Sattler. Homotopy canonicity of homotopy type theory. Talk at the International Conference on Homotopy Type Theory (HoTT 2019), Pittsburgh, given by Christian Sattler. Slides: https://hott.github.io/HoTT-2019/conf-slides/ Sattler.pdf, 2019

    2019

  31. [39]

    Extensional concepts in intensional type theory, re- visited.Theoretical Computer Science, 1029:115051, 2025

    Krzysztof Kapulkin and Yufeng Li. Extensional concepts in intensional type theory, re- visited.Theoretical Computer Science, 1029:115051, 2025. doi: 10.1016/j.tcs.2024.115051. arXiv:2310.05706

    2025

  32. [40]

    The simplicial model of univalent foundations (after Voevodsky).Journal of the European Mathematical Society, 23(6):2071– 2126, 2021

    Krzysztof Kapulkin and Peter LeFanu Lumsdaine. The simplicial model of univalent foundations (after Voevodsky).Journal of the European Mathematical Society, 23(6):2071– 2126, 2021. doi: 10.4171/jems/1050

    doi

  33. [41]

    The arend proof assistant

    JetBrains Research. The arend proof assistant. https://arend-lang.github.io/, 2019. First release (v1.0.0) July 2019. Source:https://github.com/JetBrains/Arend

    2019

  34. [42]

    Staged compilation with two-level type theory

    Andr´ as Kov´ acs. Staged compilation with two-level type theory. InICFP, volume 6 ofProceedings of the ACM on Programming Languages, pages 540–569. Association for Computing Machinery, 2022. doi: 10.1145/3547641

    2022 doi

  35. [43]

    Representing type theories in two-level type theory

    Nicolai Kraus and Tom de Jong. Representing type theories in two-level type theory. InTYPES 2025, Glasgow, UK, 2025. Available at https://msp.cis.strath.ac.uk/ types2025/abstracts/TYPES2025_paper42.pdf

    2025

  36. [44]

    Formalizing the ∞-categorical Yoneda lemma

    Nikolai Kudasov, Emily Riehl, and Jonathan Weinberger. Formalizing the ∞-categorical Yoneda lemma. In Amin Timany, Dmitriy Traytel, Brigitte Pientka, and Sandrine Blazy, editors,Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ...

    2024

  37. [45]

    Rzk proof assistant

    Nikolai Kudasov et al. Rzk proof assistant. First release (v0.1.0) March 2023. https: //github.com/rzk-lang/rzk, 2023

    2023

  38. [46]

    Displayed type theory and semi-simplicial types.Mathematical Structures in Computer Science, 35:e34, 2025

    Astra Kolomatskaia and Michael Shulman. Displayed type theory and semi-simplicial types.Mathematical Structures in Computer Science, 35:e34, 2025. doi: 10.1017/ Extension Types for Free: Cofibrations, Gluing, and Univalence in Two-Level Type Theory 27 S096012952510025X. arXiv:...

    2025

  39. [47]

    Licata, Ian Orton, Andrew M

    Daniel R. Licata, Ian Orton, Andrew M. Pitts, and Bas Spitters. Internal Universes in Models of Homotopy Type Theory. In H´ el` ene Kirchner, editor,3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), volume 108 ofLeibniz International ...

    2018

  40. [48]

    Semantics of higher inductive types

    Peter LeFanu Lumsdaine and Michael Shulman. Semantics of higher inductive types. Mathematical Proceedings of the Cambridge Philosophical Society, 169(1):159–208, 2020. doi: 10.1017/S030500411900015X

    2020 doi

  41. [49]

    ∞-type theories.Higher Structures, 9(1):179–226,

    Hoang Kim Nguyen and Taichi Uemura. ∞-type theories.Higher Structures, 9(1):179–226,

  42. [50]

    Transpension: The right adjoint to the pi-type

    Andreas Nuyts and Dominique Devriese. Transpension: The right adjoint to the pi-type. Logical Methods in Computer Science, 20(2):16:1–16:54, 2024. doi: 10.46298/lmcs-20(2: 16)2024

    2024 doi

  43. [51]

    Daniel R. Licata. weak univalence with “beta” implies full univalence. Message of 7 September to the Homotopy Type Theory mailing list, 2016. https://groups.google. com/g/homotopytypetheory/c/j2KBIvDw53s

    2016

  44. [52]

    Ian Orton and Andrew M. Pitts. Decomposing the univalence axiom. In Andreas Abel, Fredrik Nordvall Forsberg, and Ambrus Kaposi, editors,23rd International Conference on Types for Proofs and Programs (TYPES 2017), volume 104 ofLeibniz International Proceedings in Informatics (L...

    2017 doi

  45. [53]

    Extensionality in the calculus of constructions

    Nicolas Oury. Extensionality in the calculus of constructions. In Joe Hurd and Thomas F. Melham, editors,Theorem Proving in Higher Order Logics (TPHOLs 2005), volume 3603 of Lecture Notes in Computer Science, pages 278–293. Springer, 2005. doi: 10.1007/11541868 18

    2005 doi

  46. [54]

    Strictly associative group theory using univalence

    Alex Rice. Strictly associative group theory using univalence. Abstract, Workshop on Homotopy Type Theory / Univalent Foundations (HoTT/UF 2023), Vienna, Austria, 2023. Available athttps://hott-uf.github.io/2023/HoTTUF_2023_paper_5827.pdf

    2023

  47. [55]

    A type theory for synthetic ∞-categories.Higher Structures, 1(1):147–224, 2017

    Emily Riehl and Michael Shulman. A type theory for synthetic ∞-categories.Higher Structures, 1(1):147–224, 2017. doi: 10.21136/hs.2017.06

    2017 doi

  48. [56]

    doi: 10.21136/HS.2025.04

    2025 doi

  49. [57]

    PhD thesis, University of Oxford, 1986

    Giuseppe Rosolini.Continuity and Effectiveness in Topoi. PhD thesis, University of Oxford, 1986

    1986

  50. [58]

    Ian Orton and Andrew M. Pitts. Axioms for modelling cubical type theory in a topos. Logical Methods in Computer Science, 14(4), 2018. doi: 10.23638/LMCS-14(4:23)2018

    2018 doi

  51. [59]

    Do cubical models of type theory also model homotopy types? Lecture at the Hausdorff Trimester ProgramTypes, Sets and Constructions, Bonn

    Christian Sattler. Do cubical models of type theory also model homotopy types? Lecture at the Hausdorff Trimester ProgramTypes, Sets and Constructions, Bonn. Recording: https://www.youtube.com/watch?v=wkPDyIGmEoA, 2018

    2018

  52. [60]

    Towards facett: a generalization of intensional type systems with glue

    Tex Sch¨ onlank, Andreas Nuyts, and Dominique Devriese. Towards facett: a generalization of intensional type systems with glue. InTYPES 2026, Gothenburg, Sweden, 2026. Available athttps://types2026.cse.chalmers.se/abstracts/42.pdf

    2026

  53. [61]

    Univalence for inverse diagrams and homotopy canonicity.Mathematical Structures in Computer Science, 25(5):1203–1277, 2015

    Michael Shulman. Univalence for inverse diagrams and homotopy canonicity.Mathematical Structures in Computer Science, 25(5):1203–1277, 2015. doi: 10.1017/S0960129514000565

    2015 doi

  54. [62]

    All ( ∞, 1)-toposes have strict univalent universes

    Michael Shulman. All ( ∞, 1)-toposes have strict univalent universes. arXiv:1904.07004, 2019

    1904 arXiv

  55. [63]

    Cambridge Studies in Advanced Mathematics

    Egbert Rijke.Introduction to Homotopy Type Theory. Cambridge Studies in Advanced Mathematics. Cambridge University Press, 2025

    2025

  56. [64]

    Logical relations as types: Proof-relevant parametricity for program modules.Journal of the ACM (JACM), 68(6):1–47, 2021

    Jonathan Sterling and Robert Harper. Logical relations as types: Proof-relevant parametricity for program modules.Journal of the ACM (JACM), 68(6):1–47, 2021. doi: 10.1145/3474834

    2021 doi

  57. [65]

    The equivalence extension property and model structures

    Christian Sattler. The equivalence extension property and model structures. arXiv:1704.06911, 2017. 28 NICOLAI KRAUS

    2017 arXiv

  58. [66]

    redtt: a proof assistant for Cartesian cubical type theory

    The RedPRL Development Team. redtt: a proof assistant for Cartesian cubical type theory. https://github.com/RedPRL/redtt, 2018

    2018

  59. [67]

    The RedPRL Development Team. cooltt. https://github.com/RedPRL/cooltt, 2019. Repository created December 2019; rolling releases

    2019

  60. [68]

    Orthogonality closure properties, 2026

    Samuel Toth. Orthogonality closure properties, 2026. URL https://samtoth.github.io/ agda-synthetic-categories/stt-00BZ/index.xml

    2026

  61. [69]

    A general framework for the semantics of type theory.Mathematical Structures in Computer Science, 33(3):134–179, 2023

    Taichi Uemura. A general framework for the semantics of type theory.Mathematical Structures in Computer Science, 33(3):134–179, 2023. doi: 10.1017/S0960129523000208

    2023 doi

  62. [70]

    PhD thesis, Carnegie Mellon University, 2021

    Jonathan Sterling.First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory. PhD thesis, Carnegie Mellon University, 2021. CMU-CS-21-142; revised version 2022

    2021

  63. [71]

    2LTT-Agda: Formalization of 2LTT in Agda

    Elif Uskuplu. 2LTT-Agda: Formalization of 2LTT in Agda. https://github.com/ ElifUskuplu/2LTT-Agda, 2023

    2023

  64. [72]

    Andrew W. Swan. An algebraic weak factorisation system on 01-substitution sets: a constructive proof.Journal of Logic & Analysis, 8(1):1–35, 2016. doi: 10.4115/jla.2016.8.1

    2016 doi

  65. [73]

    Cubical Agda: a dependently typed programming language with univalence and higher inductive types.Proceedings of the ACM on Programming Languages, 3(ICFP):1–29, 2019

    Andrea Vezzosi, Anders M¨ ortberg, and Andreas Abel. Cubical Agda: a dependently typed programming language with univalence and higher inductive types.Proceedings of the ACM on Programming Languages, 3(ICFP):1–29, 2019. doi: 10.1145/3341691

    2019 doi

  66. [74]

    A simple type system with two identity types

    Vladimir Voevodsky. A simple type system with two identity types. Unpublished note, avail- able at https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/ HTS.pdf, 2013

    2013

  67. [75]

    Strict stability of extension types.Theory and Applications of Categories, 45(38):1555–1582, 2026

    Jonathan Weinberger. Strict stability of extension types.Theory and Applications of Categories, 45(38):1555–1582, 2026

    2026

  68. [76]

    PhD thesis, Universit´ e de Nantes, 2020.https://theses.fr/2020NANT4012

    Th´ eo Winterhalter.Formalisation and meta-theory of type theory. PhD thesis, Universit´ e de Nantes, 2020.https://theses.fr/2020NANT4012

    2020

  69. [77]

    https://homotopytypetheory.org/book, Institute for Advanced Study, 2013

    The Univalent Foundations Program.Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013

    2013

  70. [78]

    Three non-cubical applications of extension types

    Tesla Zhang. Three non-cubical applications of extension types. arXiv:2311.05658, 2023

    2023 arXiv

  71. [79]

    Formalizing two-level type theory with cofibrant exo-nat.Mathematical Struc- tures in Computer Science, 35:e30, 2025

    Elif Uskuplu. Formalizing two-level type theory with cofibrant exo-nat.Mathematical Struc- tures in Computer Science, 35:e30, 2025. doi: 10.1017/S0960129525100297. arXiv:2309.09395

    2025

  72. [84]

    Eliminating reflection from type theory

    Th´ eo Winterhalter, Matthieu Sozeau, and Nicolas Tabareau. Eliminating reflection from type theory. InProceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2019), pages 91–103. ACM, 2019. doi: 10.1145/3293880.3294095

    2019

  73. [86]

    The aya prover

    Tesla Zhang et al. The aya prover. https://www.aya-prover.org/, 2021. First release (v0.1) January 2021. Source:https://github.com/aya-prover/aya-dev

    2021

  74. [2014]

    doi: 10.4230/LIPIcs.TYPES.2013.107

    2013 doi

  75. [2018]

    ISBN 978-3-95977-077-4

    Schloss Dagstuhl – Leibniz-Zentrum f¨ ur Informatik. ISBN 978-3-95977-077-4. doi: 10.4230/LIPIcs.FSCD.2018.22. URL https://drops.dagstuhl.de/entities/document/ 10.4230/LIPIcs.FSCD.2018.22

    2018 doi

  76. [2023]

    doi: 10.4230/LIPIcs.FSCD.2023.18

    2023 doi

  77. [2025]

    doi: 10.1017/S0960129525100327

    doi

  78. [2026]

    doi: 10.1016/j.aim.2026.110965

    2026

Pith tools

Reviewed August 1, 2026 · model on record in the stance chip above.