Pith. sign in

REVIEW 4 minor 63 references

Contravariant families in simplicial type theory give the coherent expansion lemma that makes proof-relevant logical relations work with directed reductions, yielding directed Boolean canonicity.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

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

T0 review · grok-4.5

2026-07-10 12:12 UTC pith:N3YZ6ROY

load-bearing objection Solid, mechanized directed gluing that turns simplicial contravariance into proof-relevant expansion and delivers Boolean canonicity.

arxiv 2607.08154 v1 pith:N3YZ6ROY submitted 2026-07-09 cs.LO cs.PL

Directed proof-relevant logical relations in simplicial HoTT

Runming Li , Harrison Grodin , Robert Harper This is my paper
classification cs.LO cs.PL MSC 03B3818N6068N18
keywords logical relationssimplicial homotopy type theorycontravariant familiesdirected quotient inductive typescanonicitygluingparametricityflat modality
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

Ordinary proof-relevant logical relations work over syntax quotiented by equality, so they do not see the directed steps of reduction. This paper rebuilds the syntax as a directed quotient inductive type whose reductions are inequality types, then shows that the already-available notion of a contravariant family is exactly the coherent, proof-relevant form of closure under expansion. Computability evidence can therefore be transported backward along reductions with functoriality and a universal property built in. The resulting unary gluing model proves that every closed Boolean term reduces to true or false. The same pattern scales to dependent types and universes once a flat modality supplies the needed discreteness, and to binary relations once vertical reductions are separated from horizontal parametricity witnesses.

Core claim

Contravariance is proof-relevant closure under expansion. Once every computability predicate is required to be a contravariant family, the fundamental theorem of a unary logical-relations model over directed quotient syntax yields directed Boolean canonicity: every closed Boolean term M satisfies M ≤ true or M ≤ false.

What carries the argument

Contravariant families (and their induced transport maps f*): for a family C, every inequality f : x ≤ y and every value in C(y) has a unique lift in C(x) lying over f. That unique lift is the expansion map used by the logical relation; its universal property turns the directed β-laws into reflexivity of equality of witnesses.

Load-bearing premise

The raw directed higher-inductive syntax must reflect into the subuniverse of thin Segal sets so that reductions compose uniquely and remain proof-irrelevant; without that localization the mapping-out principle the model relies on fails.

What would settle it

Exhibit a closed Boolean term in the directed syntax that is well-typed yet neither reduces to true nor to false under the inequality constructors, or show that no contravariant family can interpret the product or Boolean clauses while validating the directed β-laws.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • Directed Boolean canonicity becomes a formal theorem of a gluing model rather than an external operational argument.
  • Dependent types and universes can be handled by the same method once flat codes supply discreteness for conversion and candidates.
  • Binary logical relations can keep vertical reduction separate from horizontal parametricity, giving a proof-relevant account of representation independence.
  • The same expansion structure is available off-the-shelf for any type former once its predicate is shown to be contravariant.

Where Pith is reading between the lines

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

  • A directed form of synthetic Tait computability should be obtainable by requiring the relevant extension types in the gluing topos to be contravariant.
  • The thin-Segal localization used for syntax is the free preorder on the raw directed graph of reductions; any richer proof-relevant reduction theory would need a different reflector.
  • The flat modality used for universe predicates is the same discreteness tool needed whenever a logical relation must compare predicates on types related only by reduction.
  • Phase distinctions that place equalities in one phase and inequalities out of it could recover ordinary judgmental conversion without erasing directed structure.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

0 major / 4 minor

Summary. The paper develops directed proof-relevant logical relations in simplicial homotopy type theory. Object syntax is presented as a directed quotient inductive-inductive type whose reductions are inequality constructors; each type is interpreted by a contravariant computability family, so that the universal property of contravariant transport supplies the coherent expansion lemma. For the simply-typed fragment the construction yields a unary gluing model and directed Boolean canonicity (every closed Boolean reduces to true or false). The same pattern is extended, via the flat modality and a discTy constructor, to dependent types and universes, and is sketched for binary parametricity that separates vertical reduction from horizontal relatedness. Sections 2–3 are mechanized in Cubical Agda.

Significance. If the construction is correct, the paper supplies a clean type-theoretic internalization of the classical expansion lemma that has been missing from equational gluing arguments. Identifying isContrav with proof-relevant expansion, and obtaining the directed-quotient mapping-out obligations as reflexivity via the universal property of transport, is a genuine conceptual contribution. The Cubical Agda mechanization of the simply-typed fragment (syntax, contravariance, products, functions, Booleans, and the canonicity diagram) is a concrete strength that makes the central claim checkable. The dependent/universe and binary extensions, while not fully mechanized, indicate a scalable method and give a new application of simplicial type theory outside synthetic ∞-category theory.

minor comments (4)
  1. Several typographical slips remain (e.g. “Ineqalities”, “menifested”, “mechnization”, “op. cit.” used without a clear referent). A light copy-edit pass would remove them.
  2. The localization of the raw directed HIT into thin Segal sets (Appendix A) is standard but is only sketched; a one-sentence pointer to the precise localization modality used in the Cubical library would help readers who wish to re-run the mechanization.
  3. Section 4’s use of discTy and the flat modality is clear at a high level, but the interaction between discTy and the thin-truncation constructors could be stated more explicitly so that readers see immediately that Ty remains discrete after localization.
  4. The binary queue example in Section 5 is illustrative but the relation R is only defined; a short remark that the remaining QUEUE components follow the same pattern as the unary case would make the example self-contained.

Circularity Check

0 steps flagged

No significant circularity: canonicity follows by initiality of the directed QIIT into a freely constructed gluing model whose Bool predicate is defined independently as reduction to a canonical value.

full rationale

The derivation is the standard free-model + fundamental-theorem pattern of proof-relevant gluing, adapted to directed inequalities. Syntax is the initial directed QIIT (Section 2); the gluing model equips each type with an independently defined contravariant family (Definition 3.1, Lemma 3.6 for representables); the Bool predicate is literally ∑b M ≤ ⌈b⌉ (Section 3.4); the fundamental theorem is the unique map out of the initial model, yielding the witness (diagram in 3.4.1). Nothing in the definition of the predicates or of isContrav presupposes the canonicity statement. Self-citations (equational gluing, Riehl–Shulman, flat modality) supply background infrastructure that is either mechanized or standard and do not encode the directed result. The localization to thin Segal sets (Appendix A) is the ordinary orthogonality reflector; once applied, mapping-out is well-defined by construction of the reflector, not by assuming the theorem. Score 1 only for the presence of ordinary self-citations that are not load-bearing for the central claim.

Axiom & Free-Parameter Ledger

0 free parameters · 4 axioms · 2 invented entities

The paper works entirely inside an existing foundation (simplicial HoTT + flat modality) and constructs syntax and models from it; free parameters are absent. The main external commitments are the axioms of the directed interval, thinness/Segal localization, and flat discreteness.

axioms (4)
  • standard math Existence of a directed interval 2 with endpoints i0 ≤ i1 and the resulting inequality types (Definition 2.1).
    Taken from Riehl–Shulman simplicial HoTT; used throughout to internalize reduction.
  • standard math Flat modality ♭ is an idempotent comonad whose counit is an equivalence precisely on discrete types (Axiom 4.4 / Gratzer et al.).
    Required for storing universe and type predicates so that inequalities of predicates collapse to equalities (Section 4.2).
  • domain assumption The three localization maps (circle, Arr(!), inner horn) generate a reflective subuniverse of thin Segal sets (Appendix A).
    Needed so that the directed QIIT syntax has unique composites of reductions and proof-irrelevant inequalities.
  • standard math Meta-language Booleans are discrete (Example 4.2).
    Standard axiom of simplicial type theory; used for the Boolean canonicity predicate.
invented entities (2)
  • Directed quotient inductive-inductive type (directed QIIT) for object syntax no independent evidence
    purpose: Generate contexts, types and terms together with directed reduction constructors while remaining a set/thin/Segal type.
    Syntactic sugar for ordinary HITs involving the directed interval plus localization; no independent external evidence required beyond the construction itself.
  • Flat predicate codes Pred(A°) and Cand(A°) no independent evidence
    purpose: Store computability predicates under ♭ so that universe transport and type conversion remain well-defined.
    Derived from the flat modality; the only novelty is their use inside the gluing records.

pith-pipeline@v1.1.0-grok45 · 42266 in / 2413 out tokens · 34538 ms · 2026-07-10T12:12:32.880358+00:00 · methodology

0 comments
read the original abstract

Intrinsically-typed presentations of type theory often use equality in the meta-language to represent object-language judgmental equality. In such equational syntax, proof-relevant logical relations define computability predicates on judgmental equivalence classes of types and terms. This approach, however, does not directly account for reduction, which is directed and plays a central role in many logical-relations arguments. This paper develops a directed version of proof-relevant logical relations in simplicial homotopy type theory, where reductions are internalized as \emph{inequality types}. We construct object syntax as a directed quotient inductive type. The central observation is that contravariant families in simplicial type theory provide exactly the proof-relevant form of closure under expansion for logical relations: computability evidence can be transported backward along reductions, with the required functoriality and universal property built in. Using this observation, we construct a unary logical relations model with contravariant computability predicates and prove directed Boolean canonicity: every closed Boolean term reduces to either true or false. We then extend the construction to dependent types and universes, where a comonadic flat modality provides the discreteness needed for type conversion and universe predicates. Finally, we adapt the method to binary logical relations, separating vertical reduction from horizontal parametricity and obtaining a proof-relevant account of representation independence.

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

63 extracted references · 63 canonical work pages · 7 internal anchors

  1. [1]

    Mathematical Structures in Computer Science33, 10 (2023), 868–912

    Bicategorical type theory: semantics and syntax. Mathematical Structures in Computer Science33, 10 (2023), 868–912. https://doi.org/10.1017/S0960129523000312 Stuart Allen. 1987.A Non-Type-Theoretic Semantics For Type-Theoretic Language. Ph. D. Dissertation. Cornell University. https://hdl.handle.net/1813/6706 Thorsten Altenkirch, Paolo Capriotti, Gabe Dij...

    work page doi:10.1017/s0960129523000312 2023

  2. [2]

    InProceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(St

    Type theory in type theory using quotient inductive types. InProceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(St. Petersburg, FL, USA) (POPL ’16). Association for Computing Machinery, New York, NY, USA, 18–29. https://doi.org/10.1145/2837614.2837638 Thorsten Altenkirch and Ambrus Kaposi

    work page doi:10.1145/2837614.2837638

  3. [3]

    https://doi.org/10.23638/LMCS-13(4:1)2017 Thorsten Altenkirch, Conor McBride, and Wouter Swierstra

    Normalisation by Evaluation for Type Theory, in Type Theory.Logical Methods in Computer Science13, 4 (2017). https://doi.org/10.23638/LMCS-13(4:1)2017 Thorsten Altenkirch, Conor McBride, and Wouter Swierstra

    work page doi:10.23638/lmcs-13(4:1)2017 2017

  4. [4]

    InProceedings of the 2007 Workshop on Programming Languages Meets Program Verification(Freiburg, Germany)(PLPV ’07)

    Observational equality, now!. InProceedings of the 2007 Workshop on Programming Languages Meets Program Verification(Freiburg, Germany)(PLPV ’07). Association for Computing Machinery, New York, NY, USA, 57–68. https://doi.org/10.1145/1292597.1292608 Carlo Angiuli. 2019.Computational Semantics of Cartesian Cubical Type Theory. Ph. D. Dissertation. Carnegie...

    work page doi:10.1145/1292597.1292608 2007

  5. [5]

    https://doi.org/10.1017/S0960129521000347 César Bardomiano-Martínez

    Syntax and models of Cartesian cubical type theory.Mathematical Structures in Computer Science31, 4 (2021), 424–468. https://doi.org/10.1017/S0960129521000347 César Bardomiano-Martínez

    work page doi:10.1017/s0960129521000347 2021

  6. [6]

    https://doi.org/10.1017/S0960129525100339 arXiv:2407.18072 [math.CT] Rafaël Bocquet, Ambrus Kaposi, and Christian Sattler

    Exponentiable functors between synthetic ∞-categories.Mathematical Structures in Computer Science(2025). https://doi.org/10.1017/S0960129525100339 arXiv:2407.18072 [math.CT] Rafaël Bocquet, Ambrus Kaposi, and Christian Sattler

    work page doi:10.1017/s0960129525100339 2025

  7. [7]

    260), Marco Gaboardi and Femke van Raamsdonk (Eds.)

    (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 260), Marco Gaboardi and Femke van Raamsdonk (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 18:1–18:23. https://doi.org/10.4230/LIPIcs.FSCD.2023.18 Ulrik Buchholtz and Jonathan Weinberger

    work page doi:10.4230/lipics.fscd.2023.18 2023

  8. [8]

    https://doi.org/10.21136/HS.2023.04 Evan Cavallo, Emily Riehl, and Christian Sattler

    Synthetic fibered (∞, 1)-category theory.Higher Structures7, 1 (2023), 74–165. https://doi.org/10.21136/HS.2023.04 Evan Cavallo, Emily Riehl, and Christian Sattler

    work page doi:10.21136/hs.2023.04 2023

  9. [9]

    Directed univalence for simplicial objects in an $\infty$-topos

    Directed univalence for simplicial objects in an ∞-topos. arXiv:2607.02420 [math.CT] https://arxiv.org/abs/2607.02420 Liang-Ting Chen, Fredrik Nordvall Forsberg, and Tzu-Chun Tsai

    work page internal anchor Pith review Pith/arXiv arXiv

  10. [10]

    InProceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs(Rennes, France)(CPP ’26)

    Can We Formalise Type Theory Intrinsically without Any Compromise? A Case Study in Cubical Agda. InProceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs(Rennes, France)(CPP ’26). Association for Computing Machinery, New York, NY, USA, 201–215. https://doi.org/10.1145/3779031.3779090 J. Daniel Christensen, Morgan Opi...

    work page doi:10.1145/3779031.3779090

  11. [11]

    2020), 1–32

    Localization in Homotopy Type Theory.Higher Structures4 (Feb. 2020), 1–32. Issue

    work page 2020

  12. [12]

    https://doi.org/10.21136/HS.2020.01 Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg

    work page doi:10.21136/hs.2020.01 2020

  13. [13]

    69), Tarmo Uustalu (Ed.)

    (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 69), Tarmo Uustalu (Ed.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 5:1–5:34. https://doi.org/10.4230/LIPIcs.TYPES.2015.5 Robert L. Constable, Stuart F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, T. B. Knoblock, N. P. ...

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

  14. [14]

    Canonicity and normalisation for Dependent Type Theory

    Canonicity and normalisation for Dependent Type Theory. arXiv:1810.09367 [cs.PL] https: //arxiv.org/abs/1810.09367 Thierry Coquand, Simon Huber, and Christian Sattler

    work page internal anchor Pith review Pith/arXiv arXiv

  15. [15]

    131), Herman Geuvers (Ed.)

    (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 131), Herman Geuvers (Ed.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 11:1–11:23. https://doi.org/10.4230/LIPIcs.FSCD.2019.11 28 Runming Li, Harrison Grodin, and Robert Harper Peter Dybjer

    work page doi:10.4230/lipics.fscd.2019.11 2019

  16. [16]

    InProceedings of the 4th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP ’02)

    Semantic analysis of normalisation by evaluation for typed lambda calculus. InProceedings of the 4th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP ’02). Association for Computing Machinery, 26–37. https://doi.org/10.1145/571157.571161 Marcelo P. Fiore

    work page doi:10.1145/571157.571161

  17. [17]

    Mathematical Structures in Computer Science7, 5 (Oct

    An Enrichment Theorem for an Axiomatisation of Categories of Domains and Continuous Functions. Mathematical Structures in Computer Science7, 5 (Oct. 1997), 591–618. https://doi.org/10.1017/S0960129597002429 Daniel Gratzer

    work page doi:10.1017/s0960129597002429 1997

  18. [18]

    InProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science

    Normalization for Multimodal Type Theory. InProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science. ACM, Haifa Israel, 1–13. https://doi.org/10.1145/3531130.3532398 Daniel Gratzer. 2023.Syntax and Semantics of Modal Type Theory. Ph. D. Dissertation. Aarhus University. https://www. danielgratzer.com/papers/phd-thesis.pdf Daniel Grat...

    work page doi:10.1145/3531130.3532398 2023

  19. [19]

    ACM Program

    Abstraction Functions as Types: Modular Verification of Cost and Behavior in Dependent Type Theory.Proc. ACM Program. Lang.10, POPL, Article 31 (Jan. 2026), 28 pages. https: //doi.org/10.1145/3776673 Harrison Grodin, Yue Niu, Jonathan Sterling, and Robert Harper

    work page doi:10.1145/3776673 2026

  20. [20]

    ACM Program

    Decalf: A Directed, Effectful Cost-Aware Logical Framework.Proc. ACM Program. Lang.8, POPL, Article 10 (Jan. 2024), 29 pages. https://doi.org/10.1145/3632852 Robert Harper

    work page doi:10.1145/3632852 2024

  21. [21]

    https://doi.org/10.1016/0747-7171(92)90026-Z Robert Harper

    Constructing Type Systems over an Operational Semantics.Journal of Symbolic Computation14, 1 (1992), 71–84. https://doi.org/10.1016/0747-7171(92)90026-Z Robert Harper

    work page doi:10.1016/0747-7171(92)90026-z 1992

  22. [22]

    An Equational Logical Framework for Type Theories

    An Equational Logical Framework for Type Theories. https://arxiv.org/abs/2106.01484 Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, and Derek Dreyer

    work page internal anchor Pith review Pith/arXiv arXiv

  23. [23]

    2018), e20

    Iris from the ground up: A modular foundation for higher-order concurrent separation logic.Journal of Functional Programming28 (Nov. 2018), e20. https://doi.org/10.1017/S0956796818000151 Ambrus Kaposi, Simon Huber, and Christian Sattler. 2019a. Gluing for Type Theory. In4th International Conference on Formal Structures for Computation and Deduction (FSCD

    work page doi:10.1017/s0956796818000151 2018

  24. [24]

    131), Herman Geuvers (Ed.)

    (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 131), Herman Geuvers (Ed.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 25:1–25:19. https://doi.org/10.4230/LIPIcs.FSCD.2019.25 Ambrus Kaposi, András Kovács, and Thorsten Altenkirch. 2019b. Constructing quotient inductive-inductive types.Proc. ACM Program. Lang.3, P...

    work page doi:10.4230/lipics.fscd.2019.25 2019

  25. [25]

    ACM Program

    Type Theory in Type Theory using a Strictified Syntax.Proc. ACM Program. Lang. ICFP (Aug. 2025), 31 pages. https://doi.org/10.1145/3747535 András Kovács

    work page doi:10.1145/3747535 2025

  26. [26]

    ACM Program

    Canonicity for Indexed Inductive-Recursive Types.Proc. ACM Program. Lang.10, POPL, Article 43 (Jan. 2026), 29 pages. https://doi.org/10.1145/3776685 Neelakantan R. Krishnaswami and Derek Dreyer

    work page doi:10.1145/3776685 2026

  27. [27]

    InComputer Science Logic 2013 (CSL

    Internalizing Relational Parametricity in the Extensional Calculus of Constructions. InComputer Science Logic 2013 (CSL

    work page 2013

  28. [28]

    23), Simona Ronchi Della Rocca (Ed.)

    (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 23), Simona Ronchi Della Rocca (Ed.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 432–451. https://doi.org/10.4230/LIPIcs.CSL.2013.432 Nikolai Kudasov

    work page doi:10.4230/lipics.csl.2013.432 2013

  29. [29]

    InProceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs(London, UK)(CPP 2024)

    Formalizing the∞-Categorical Yoneda Lemma. InProceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs(London, UK)(CPP 2024). Association for Computing Machinery, New York, NY, USA, 274–290. https://doi.org/10.1145/3636501.3636945 Andrea Laretto, Fosco Loregian, and Niccolò Veltri

    work page doi:10.1145/3636501.3636945 2024

  30. [30]

    ACM Program

    Di- is for Directed: First-Order Directed Type Theory via Dinaturality.Proc. ACM Program. Lang.10, POPL, Article 61 (Jan. 2026), 31 pages. https://doi.org/10.1145/3776703 Runming Li and Robert Harper

    work page doi:10.1145/3776703 2026

  31. [31]

    Canonicity for Cost-Aware Logical Framework via Synthetic Tait Computability

    Canonicity for Cost-Aware Logical Framework via Synthetic Tait Computability. arXiv:2504.12464 (April 2025). https://doi.org/10.48550/arXiv.2504.12464 arXiv:2504.12464 [cs]. Runming Li, Yue Yao, and Robert Harper

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2504.12464 2025

  32. [32]

    InProceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs(Rennes, France)(CPP ’26)

    Mechanizing Synthetic Tait Computability in Istari. InProceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs(Rennes, France)(CPP ’26). Association for Computing Machinery, New York, NY, USA, 231–247. https://doi.org/10.1145/3779031.3779085 Directed proof-relevant logical relations in simplicial HoTT 29 Daniel R. Lica...

    work page doi:10.1145/3779031.3779085

  33. [33]

    https://doi.org/10.1016/j.entcs.2011.09.026 Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVII)

    2-Dimensional Directed Type Theory.Electronic Notes in Theoretical Computer Science276 (2011), 263–289. https://doi.org/10.1016/j.entcs.2011.09.026 Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVII). Daniel R. Licata, Ian Orton, Andrew M. Pitts, and Bas Spitters

    work page doi:10.1016/j.entcs.2011.09.026 2011

  34. [34]

    108), Hélène Kirchner (Ed.)

    (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 108), Hélène Kirchner (Ed.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 22:1–22:17. https://doi.org/10.4230/LIPIcs.FSCD.2018.22 Per Martin-Löf

    work page doi:10.4230/lipics.fscd.2018.22 2018

  35. [35]

    Preliminary version 1972; reprinted version of an unpublished report from

    Oxford University Press, New York, NY, USA, 127–172. Preliminary version 1972; reprinted version of an unpublished report from

    work page 1972

  36. [36]

    InSelected Papers from the Workshop on Computer Science Logic (CSL ’92)

    Notes on Sconing and Relators. InSelected Papers from the Workshop on Computer Science Logic (CSL ’92). Springer-Verlag, Berlin, Heidelberg, 352–378. Jacob Neumann. 2025a.A Generalized Algebraic Theory of Directed Equality. Ph. D. Dissertation. University of Nottingham. Jacob Neumann. 2025b. A Judgmental Construction of Directed Type Theory. arXiv:2510.17...

    work page arXiv

  37. [37]

    https://doi.org/10.4230/LIPICS.TYPES.2024.7 Yue Niu, Jonathan Sterling, Harrison Grodin, and Robert Harper

    Synthetic 1-Categories in Directed Type Theory.LIPIcs, Volume 336, TYPES 2024336, 7:1–7:23. https://doi.org/10.4230/LIPICS.TYPES.2024.7 Yue Niu, Jonathan Sterling, Harrison Grodin, and Robert Harper

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

  38. [38]

    ACM Program

    A cost-aware logical framework.Proc. ACM Program. Lang.6, POPL, Article 9 (Jan. 2022), 31 pages. https://doi.org/10.1145/3498670 Ulf Norell

    work page doi:10.1145/3498670 2022

  39. [39]

    InProceedings of the 4th International Workshop on Types in Language Design and Implementation (TLDI ’09)

    Dependently Typed Programming in Agda. InProceedings of the 4th International Workshop on Types in Language Design and Implementation (TLDI ’09). Association for Computing Machinery, New York, NY, USA, 1–2. https://doi.org/10.1145/1481861.1481862 Paige Randall North

    work page doi:10.1145/1481861.1481862

  40. [40]

    https://doi.org/10.1016/j.entcs.2019.09.012 Proceedings of the Thirty-Fifth Conference on the Mathematical Foundations of Programming Semantics

    Towards a Directed Homotopy Type Theory.Electronic Notes in Theoretical Computer Science 347 (2019), 223–239. https://doi.org/10.1016/j.entcs.2019.09.012 Proceedings of the Thirty-Fifth Conference on the Mathematical Foundations of Programming Semantics. Andreas Nuyts. 2015.Towards a Directed Homotopy Type Theory based on 4 Kinds of Variance. Master’s the...

    work page doi:10.1016/j.entcs.2019.09.012 2019

  41. [41]

    2001), 511–540

    A Judgmental Reconstruction of Modal Logic.Mathematical Structures in Computer Science11, 4 (Aug. 2001), 511–540. https://doi.org/10.1017/S0960129501003322 Loïc Pujet and Nicolas Tabareau

    work page doi:10.1017/s0960129501003322 2001

  42. [42]

    ACM Program

    Observational equality: now for good.Proc. ACM Program. Lang.6, POPL, Article 32 (Jan. 2022), 27 pages. https://doi.org/10.1145/3498693 Emily Riehl and Michael Shulman

    work page doi:10.1145/3498693 2022

  43. [43]

    A type theory for synthetic ∞-categories.Higher Structures1 (2017), 147–224. Issue

    work page 2017

  44. [44]

    arXiv:1705.07442 [math.CT] https://journals.mq.edu.au/index.php/higher_structures/article/view/36 Egbert Rijke, Michael Shulman, and Bas Spitters

    work page internal anchor Pith review Pith/arXiv arXiv

  45. [45]

    https://doi.org/10.23638/LMCS-16(1:2)2020 Robert A

    Modalities in homotopy type theory.Logical Methods in Computer ScienceVolume 16, Issue 1, Article 2 (Jan 2020). https://doi.org/10.23638/LMCS-16(1:2)2020 Robert A. G. Seely

    work page doi:10.23638/lmcs-16(1:2)2020 2020

  46. [46]

    InProceedings of the Second Annual IEEE Symposium on Logic in Computer Science (LICS 1987)(Ithaca, NY, USA)

    Modelling Computations: A 2-Categorical Framework. InProceedings of the Second Annual IEEE Symposium on Logic in Computer Science (LICS 1987)(Ithaca, NY, USA). IEEE Computer Society Press, 65–71. Michael Shulman

    work page 1987

  47. [47]

    https://doi.org/10.1017/S0960129514000565 Michael Shulman

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

    work page doi:10.1017/s0960129514000565 2015

  48. [48]

    https://doi.org/10.1017/S0960129517000147 Jonathan Sterling

    Brouwer’s Fixed-Point Theorem in Real-Cohesive Homotopy Type Theory.Mathematical Structures in Computer Science28, 6 (June 2018), 856–941. https://doi.org/10.1017/S0960129517000147 Jonathan Sterling. 2021.First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory. Ph. D. Dissertation. Carnegie Mellon University. https://d...

    work page doi:10.1017/s0960129517000147 2018

  49. [49]

    36th Annual

    Normalization for Cubical Type Theory. In2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). 1–15. https://doi.org/10.1109/LICS52264.2021.9470719 Jonathan Sterling and Robert Harper

    work page doi:10.1109/lics52264.2021.9470719 2021

  50. [50]

    Logical Relations as Types: Proof-Relevant Parametricity for Program Modules. J. ACM68, 6 (Dec. 2021), 1–47. https://doi.org/10.1145/3474834 Jonathan Sterling and Robert Harper

    work page doi:10.1145/3474834 2021

  51. [51]

    228), Amy P

    (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 228), Amy P. Felty (Ed.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 5:1–5:19. https://doi.org/10. 4230/LIPIcs.FSCD.2022.5 Jonathan Sterling and Bas Spitters

    work page 2022

  52. [52]

    Normalization by gluing for free {\lambda}-theories

    Normalization by gluing for free𝜆-theories. https://arxiv.org/abs/1809.08646 W. W. Tait

    work page internal anchor Pith review Pith/arXiv arXiv

  53. [53]

    32, 2 (1967), 198–212

    Intensional Interpretations of Functionals of Finite Type I. 32, 2 (1967), 198–212. http://www.jstor.org/ stable/2271658 The Agda Team. 2026.Flat Modality. Agda. https://agda.readthedocs.io/en/latest/language/flat.html Agda 2.9.0 documenta- tion. 30 Runming Li, Harrison Grodin, and Robert Harper Constantine Theocharis and Edwin Brady

    work page arXiv 1967

  54. [54]

    Type Theory With Erasure

    Type Theory With Erasure. https://doi.org/10.48550/arXiv.2605.00655 arXiv:2605.00655 [cs.PL] Accepted to FSCD

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2605.00655

  55. [55]

    ACM 71, 6, Article 40 (Nov

    A Logical Approach to Type Soundness.J. ACM 71, 6, Article 40 (Nov. 2024), 75 pages. https://doi.org/10.1145/3676954 The Univalent Foundations Program. 2013.Homotopy Type Theory: Univalent Foundations of Mathematics. https: //homotopytypetheory.org/book, Institute for Advanced Study. Andrea Vezzosi, Anders Mörtberg, and Andreas Abel

    work page doi:10.1145/3676954 2024

  56. [56]

    https://doi.org/10.1145/3341691 Matthew Z

    Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types.Proceedings of the ACM on Programming Languages3, ICFP (July 2019), 87:1–87:29. https://doi.org/10.1145/3341691 Matthew Z. Weaver and Daniel R. Licata

    work page doi:10.1145/3341691 2019

  57. [57]

    InProceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science(Saarbrücken, Germany)(LICS ’20)

    A Constructive Model of Directed Univalence in Bicubical Sets. InProceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science(Saarbrücken, Germany)(LICS ’20). Association for Computing Machinery, New York, NY, USA, 915–928. https://doi.org/10.1145/3373718.3394794 Jonathan Weinberger. 2022.A Synthetic Perspective on (∞, 1)-Category Theory...

    work page doi:10.1145/3373718.3394794 2022

  58. [58]

    https://doi.org/10.1007/s40062-024-00348-3 Jonathan Weinberger, Benedikt Ahrens, Ulrik Buchholtz, and Paige North

    Two-sided cartesian fibrations of synthetic (∞, 1)-categories.Journal of Homotopy and Related Structures19, 2 (June 2024). https://doi.org/10.1007/s40062-024-00348-3 Jonathan Weinberger, Benedikt Ahrens, Ulrik Buchholtz, and Paige North

    work page doi:10.1007/s40062-024-00348-3 2024

  59. [59]

    Extended abstract at the 28th International Conference on Types for Proofs and Programs (TYPES 2022)

    Synthetic Tait Computability for Simplicial Type Theory. Extended abstract at the 28th International Conference on Types for Proofs and Programs (TYPES 2022). https://types22.inria.fr/files/2022/06/TYPES_2022_paper_17.pdf Szumi Xie and Viktor Bense

    work page 2022

  60. [60]

    Contributed talk at SSTT 2026, MFPS XLII & SSTT

    Formalizing type theory through transport hell. Contributed talk at SSTT 2026, MFPS XLII & SSTT

    work page 2026

  61. [61]

    2024.Structure and Language of Higher-Order Algebraic Effects

    https://ul-fmf.github.io/mfps-sstt-2026/sstt-contributed-talks/ Zhixuan Yang. 2024.Structure and Language of Higher-Order Algebraic Effects. Ph. D. Dissertation. Imperial College London. https://yangzhixuan.github.io/pdf/yang-thesis.pdf Zhixuan Yang and Nicolas Wu

    work page 2026

  62. [62]

    ACM Program

    Handling Higher-Order Effectful Operations with Judgemental Monadic Laws.Proc. ACM Program. Lang.10, POPL, Article 36 (Jan. 2026), 30 pages. https://doi.org/10.1145/3776678 Directed proof-relevant logical relations in simplicial HoTT 31 A The Orthogonality Construction This appendix records the orthogonality construction used in Section

    work page doi:10.1145/3776678 2026

  63. [63]

    The general background is the standard theory of orthogonal reflective subuniverses and localizations in homotopy type theory [Christensen et al

    in constructing types as synthetic preorders. The general background is the standard theory of orthogonal reflective subuniverses and localizations in homotopy type theory [Christensen et al. 2020; Fiore 1997; Rijke et al. 2020]. This construction is used in our Cubical Agda mechanization, making use of the localization modality as a higher inductive type...

    work page 2020