1 Introduction

Univalence is the structural principle that distinguishes homotopy type theory from intensional Martin–Löf type theory. Its statement, $$\mathsf{ua}:(A\simeq B)\stackrel{\simeq }{\to }(A{=}_{\mathcal{U}}B),$$ internalises Mac Lane’s slogan isomorphic objects are equal into the type theory itself . Once one accepts univalence, virtually every homotopy-theoretic and category-theoretic phenomenon admits a natural type-theoretic expression: equivalences become identities, transport along an equivalence is automatic, and the structure identity principle becomes a theorem rather than a methodological wish.

Yet univalence as stated lives in a fundamentally symmetric world. The identity type $A{=}_{\mathcal{U}}B$ is a groupoid: it has inverses. This reflects a basic fact about the type-theoretic universe: every type, in HoTT, is treated as an $\infty$-groupoid. Categories proper — where morphisms can be non-invertible — do not admit a clean internal description in HoTT without artefacts.

Directed type theory aims to repair this asymmetry by introducing a directed analogue of the path type, often written ${\mathsf{Hom}}_A(a,b)$, which need not be invertible. The objective is a synthetic theory of $(\infty ,1)$-categories analogous to the way HoTT serves as a synthetic theory of $\infty$-groupoids. Riehl and Shulman’s 2017 paper  introduces simplicial type theory ($\mathbf{STT}$) as such a foundation. The fundamental new ingredient is a strict interval $2$ with two distinct endpoints $0,1:2$ and a sub-type-system of topes (propositions over the cube of intervals) that lets one write extension types of the form $$⟨\prod _{t:2}A(t)\mid \Phi \mapsto a⟩,$$ the type of dependent functions on $2$ that on the tope $\Phi$ agree definitionally with a prescribed partial function $a$. Hom-types are then defined as extension types out of $2$.

Within $\mathbf{STT}$ there is no a priori guarantee that an arbitrary type $A$ describes an $(\infty ,1)$-category — only that it has a mapping space structure. Two predicates $\mathsf{isSegal}(A)$ (composition of hom-types) and $\mathsf{isRezk}(A)$ (equivalences are identities) cut out the types of interest, the Rezk types, which model complete Segal spaces and hence $(\infty ,1)$-categories.

The natural question is then: is there a directed analogue of univalence? If $\mathcal{S}$ is some directed universe of types, is the hom-type ${\mathsf{Hom}}_{\mathcal{S}}(A,B)$ equivalent to the type of functions $\mathsf{Fun}(A,B):=A\to B$? Riehl–Shulman prove a partial result: a covariant family $P:A\to \mathcal{U}$ is classified by a functor $A\to {\mathcal{S}}_{\mathsf{disc}}$ into the discrete sub-universe, and the data of the family is recovered up to equivalence from the functor. This is directed univalence for covariant families but not for the universe at large.

For seven years, the question of whether the directed universe itself satisfies a directed univalence principle was open. Gratzer, Weinberger and Buchholtz (2024) settle the question for the discrete sub-universe: they introduce a system of modalities adequate to express both the directed universe and the symmetric universe of $\infty$-groupoids inside it, and prove $${\mathsf{dua}}_{\mathcal{S}}:{\mathsf{Hom}}_{\mathcal{S}}(A,B)\simeq \mathsf{Fun}(A,B),$$ where $\mathcal{S}$ is the universe of discrete types . They name the resulting system triangulated type theory ($\mathbf{TTT}$), reflecting the appearance of a triangle of modalities $♭⊣\mathsf{Disc}⊣♯$ analogous to Schreiber–Shulman cohesion.

This paper has four aims:

1. Give a self-contained, structured account of $\mathbf{STT}$ (Section 3) and partial directed univalence (Section 4).

2. Present the Gratzer–Weinberger–Buchholtz construction (Section 5) and isolate exactly what is and is not proved.

3. Formulate four candidate complete directed univalence principles (Section 6) and analyse the obstructions.

4. Connect directed univalence to higher inductive types, $(\infty ,1)$-natural number objects, and synthetic representation theory (Section 7).

We accompany the exposition with formal sketches in Haskell (under src/) and Lean 4 (under lean/) that mechanise the relevant equivalences for the discrete fragment and lay out the directed universe API. The Haskell modules are not Lean proofs — they implement toy models that exhibit the algebraic content (covariant fibrations as $A\to \mathcal{S}$ functors, hom-types as Day convolutions on a $2$-action) so that the conceptual content can be machine-checked even if foundationally weakened. Lean 4 sketches use postulates where appropriate.

Open problems are collected in Section 9. We list four: extension to non-discrete universes, $(\infty ,1)$-Cat as a primitive type, internal language theorems for cocartesian fibrations, and the connection to Langlands.

1.0.0.1 Conventions.

We write $\mathcal{U}$ for an ambient (symmetric) universe; $\mathcal{S}$ for a directed sub-universe; $A:\mathcal{U}$ or $A:\mathcal{S}$ for a type/object; $a,b:A$ for terms. The directed interval is $2=\{0\le 1\}$. Hom-types are written ${\mathsf{Hom}}_A(a,b)$ and identity types $a{=}_{A}b$. We use $f\simeq g$ for the type of equivalences. Throughout, $\mathbf{STT}$ refers to Riehl–Shulman 2017 simplicial type theory, $\mathbf{TTT}$ to Gratzer–Weinberger–Buchholtz 2024 triangulated type theory.

2 Background: Symmetric Univalence and Directed Motivation

2.1 Voevodsky’s univalence axiom

We recall the symmetric statement, both for orientation and to highlight what breaks when one passes to the directed setting.

The axiom yields its inverse $\mathsf{ua}:(A\simeq B)\to (A{=}_{\mathcal{U}}B)$ and the computation $\mathsf{idtoeqv}\circ \mathsf{ua}\sim \mathsf{id}$. Operationally, every equivalence delivers a path in the universe, and transport along this path acts as the equivalence.

2.1.0.1 What is symmetric.

Two structural features of $A{=}_{\mathcal{U}}B$ make it manifestly symmetric:

1. It has inverses: if $p:A{=}_{\mathcal{U}}B$ then $p^{-1}:B{=}_{\mathcal{U}}A$.

2. It is recursive: $\mathsf{idtoeqv}$ may be defined by path induction, which is symmetric in $A$ and $B$.

Both features are absent in the directed setting we wish to formalise.

2.2 What “directed” should mean

A directed type theory ought to admit, for each type $A$ and pair of terms $a,b:A$, a hom-type $${\mathsf{Hom}}_A(a,b):\mathcal{U},$$ together with composition $$\circ :{\mathsf{Hom}}_A(b,c)\times {\mathsf{Hom}}_A(a,b)⟶{\mathsf{Hom}}_A(a,c)$$ and identities ${\mathsf{id}}_a:{\mathsf{Hom}}_A(a,a)$, satisfying associativity and unit laws up to higher coherent homotopy. Crucially, ${\mathsf{Hom}}_A(a,b)$ should not in general carry inverses: if it did, the theory would collapse back to a symmetric one.

We can articulate desiderata.

1. Hom is non-invertible. The composition is not in general invertible.

2. Functoriality. Functions $f:A\to B$ act on hom-types: $$f_{\ast }:{\mathsf{Hom}}_A(a,b)⟶{\mathsf{Hom}}_B(f(a),f(b)).$$

3. Equivalences are identities. For appropriately structured types, an invertible morphism in ${\mathsf{Hom}}_A(a,b)$ should yield an identity $a{=}_{A}b$.

4. Synthetic $(\infty ,1)$-category theory. The Yoneda lemma, adjoint functors, Kan extensions, and limits/colimits should be expressible synthetically on top of these primitives.

5. Directed univalence. The universe should reflect its own hom-structure: hom in the universe = function type.

(D1)–(D4) are addressed by Riehl–Shulman and the body of subsequent work . (D5) is the topic of this paper.

2.3 $(\infty ,1)$-categorical motivation

There is a clean semantic picture explaining why directed univalence is hard. In HoTT, the universe $\mathcal{U}$ is interpreted as an object classifier in an $(\infty ,1)$-topos: $\mathcal{U}$ classifies small bundles up to fibrewise equivalence. Univalence is the corresponding internal statement: equivalences of bundles are paths in $\mathcal{U}$.

The directed analogue would have a universe $\mathcal{S}$ classifying bundles up to map, not just equivalence. In an $(\infty ,1)$-topos $\mathcal{X}$, the natural such classifier is the cocartesian fibration of the $(\infty ,1)$-category ${\mathcal{X}}_{/-}$ over $\mathcal{X}$ itself. But this is no longer a single object: it is a structured presentable $(\infty ,1)$-category. The naive analogue — “a small object in $\mathcal{X}$ that classifies maps” — requires at least a handle on $\mathcal{X}$ as an $(\infty ,1)$-category internal to $\mathcal{X}$, a strictly stronger demand than internal $\infty$-groupoids.

This is the structural reason a complete directed univalence principle is hard: it forces the type theory to internalise its own large $(\infty ,1)$-categorical structure, not merely its $\infty$-groupoidal one.

3 Riehl–Shulman Simplicial Type Theory

3.1 Topes, cubes, extension types

$\mathbf{STT}$ is a three-layer system: a homotopy type theory; a strict cube layer with the directed interval $2=\{0\le 1\}$; and a tope layer of decidable propositions over the cube. We sketch each layer.

3.2 Hom-types and Segal types

So a morphism from $a$ to $b$ is a function $2\to A$ taking $0$ to $a$ and $1$ to $b$. The directed interval is ordered, hence so is the hom-type.

Segal types are the STT version of Segal complete spaces. Composition is then a definable operation: $$\circ :{\mathsf{Hom}}_A(b,c)\times {\mathsf{Hom}}_A(a,b)\to {\mathsf{Hom}}_A(a,c)$$ when $\mathsf{isSegal}(A)$.

3.3 Discrete types

3.4 Synthetic Yoneda lemma

A high point of  is a synthetic Yoneda lemma. We state it informally.

This is the engine that drives much of synthetic $(\infty ,1)$-category theory in $\mathbf{STT}$.

4 Partial Directed Univalence (Riehl–Shulman 2017)

4.1 Covariant fibrations

In semantic terms, covariant families correspond to left fibrations: functors $A\to \mathcal{S}$ classified by a particular kind of straightening.

This is directed univalence for covariant fibrations valued in discrete types: the universe ${\mathcal{S}}_{\mathsf{disc}}$ classifies covariant families, in exact analogy with $\mathcal{U}$ classifying type families up to equivalence.

4.2 What is partial about it

Theorem 16 stops short of asserting $${\mathsf{Hom}}_{\mathcal{S}}(A,B)\simeq \mathsf{Fun}(A,B)$$ for the universe $\mathcal{S}$ itself treated as a Segal type. Two reasons.

4.2.0.1 (1) The universe is not internally Segal.

In $\mathbf{STT}$ as set up by Riehl–Shulman, the discrete universe ${\mathcal{S}}_{\mathsf{disc}}$ is given as a sub-type of $\mathcal{U}$, but its hom-type ${\mathsf{Hom}}_{{\mathcal{S}}_{\mathsf{disc}}}(A,B)$ is not directly described. The straightening theorem describes covariant maps into ${\mathcal{S}}_{\mathsf{disc}}$, not the hom-type within ${\mathcal{S}}_{\mathsf{disc}}$.

4.2.0.2 (2) Modal pieces are missing.

To formulate “${\mathsf{Hom}}_{\mathcal{S}}(A,B)\simeq \mathsf{Fun}(A,B)$” coherently, one needs to mediate between the directed setting (where the universe carries non-trivial morphisms) and the symmetric setting (where it carries only equivalences). This is precisely the function of the modal apparatus of Gratzer–Weinberger–Buchholtz, which is absent from .

4.3 Limitations made formal

These limitations motivate the modal extension we now describe.

5 Triangulated Type Theory
(Gratzer–Weinberger–Buchholtz 2024)

5.1 Modal layer

The crucial new ingredient in  is a system of modalities. We describe four.

5.2 The discrete universe $\mathcal{S}$

5.3 The directed univalence theorem

5.4 Worked examples in the discrete universe

We illustrate Theorem 22 with three small examples that occupy the discrete universe $\mathcal{S}$.

5.5 Comparison to the symmetric universe

It is instructive to compare Theorem 22 with Voevodsky’s univalence (Theorem 3).

• Voevodsky: ${\mathsf{Id}}_{\mathcal{U}}(A,B)\simeq (A\simeq B)$. Identifications in the universe correspond to equivalences of types.

• GWB: ${\mathsf{Hom}}_{\mathcal{S}}(A,B)\simeq \mathsf{Fun}(A,B)$. Directed morphisms in the universe of discrete types correspond to functions of types.

In a sense, GWB is structurally simpler: $\mathsf{Fun}(A,B)$ is the standard function type, while $A\simeq B$ requires the entire equivalence apparatus. But GWB only applies to the discrete sub-universe, so the principle is local. The challenge of extending it (Section 6) is to find a richer universe in which non-equivalence functions still correspond to directed morphisms.

5.6 Implementation status in rzk

The rzk proof assistant  implements simplicial type theory with topes and extension types. It does not (as of 2026) implement triangulated modalities or prove directed univalence. Bubenik et al. are pursuing a triangulated extension; partial formalisations of the GWB theorem are in progress.

The Haskell module Hom.hs accompanying this paper exhibits a toy form of $\mathsf{funtohom}$ for the discrete universe in a Hask-like setting. The Lean 4 file Directed.lean postulates Theorem 22 as an axiom and derives small consequences.

5.7 What is and is not proved

6 Toward a Complete Principle

We now formulate four increasingly strong candidate principles and analyse what each proof would require.

6.1 Four candidates

6.2 Layered programme

We articulate a layered programme as follows. Let $L_n$ denote a universe at layer $n$. Then:

• $L_0={\mathcal{S}}_{\mathsf{disc}}$: classical directed univalence (Candidate I).

• $L_1={\mathcal{S}}_{\mathsf{Seg}}$: Segal directed univalence (Candidate II); morphisms are Segal functors.

• $L_2={\mathcal{S}}_{\mathsf{Rezk}}$: Rezk directed univalence (Candidate III); morphisms are functors of $(\infty ,1)$-categories.

• $L_3=\mathcal{U}$: universal directed univalence (Candidate IV); requires reflective sub-universe technology.

6.3 Obstructions to Candidates II–IV

6.4 Sketch of a proof attempt for Candidate III

We sketch what a proof of Candidate III would look like, identifying the gaps.

1. Define the universe ${\mathcal{S}}_{\mathsf{Rezk}}$ as the sub-type of $\mathcal{U}$ on Rezk types: ${\mathcal{S}}_{\mathsf{Rezk}}:={\sum }_{A:\mathcal{U}}\mathsf{isRezk}(A)$.

2. Show ${\mathcal{S}}_{\mathsf{Rezk}}$ is Segal in $\mathbf{TTT}$. This is plausibly an extension of Theorem 21 but requires that $\mathsf{isRezk}$ commute with extension types out of $2$, which is non-trivial.

3. Show ${\mathcal{S}}_{\mathsf{Rezk}}$ is in fact Rezk (so that “equivalences in ${\mathcal{S}}_{\mathsf{Rezk}}$ are identities”). Equivalences in this context are functors that are essentially surjective and fully faithful in the synthetic sense.

4. Construct $\mathsf{funtohom}:\mathsf{Fun}(A,B)\to {\mathsf{Hom}}_{{\mathcal{S}}_{\mathsf{Rezk}}}(A,B)$. Functions between Rezk types are functors of $(\infty ,1)$-categories.

5. Construct an inverse using a twisted modality ${\mathsf{Disc}}^{\mathsf{Rezk}}$ that picks out Rezk types as a localisation of $\mathbf{STT}$.

Step 5 is the principal technical gap. The modality ${\mathsf{Disc}}^{\mathsf{Rezk}}$ does not exist in published $\mathbf{TTT}$.

6.5 The Cisinski–Nguyen line of work

A complementary semantic line of work is due to Cisinski and Nguyen , who construct a universal cocartesian fibration for the $(\infty ,1)$-topos of presheaves of spaces. In categorical terms, this is the directed analogue of an object classifier: it is a cocartesian fibration ${\mathcal{U}}^{\to }\to \mathcal{U}$ whose fibre over $A:\mathcal{U}$ is essentially the slice ${\mathcal{U}}_{/A}$.

Translated into the directed type theory programme, Cisinski–Nguyen suggests a semantic sub-universe of $\mathcal{U}$ on which the directed-univalence statement should hold: $${\mathsf{Hom}}_{{\mathcal{U}}^{\to }}(A,B)\simeq \mathcal{U}(A,B)=\mathsf{Fun}(A,B).$$ The question is whether this sub-universe can be characterised syntactically in a directed type theory, and in particular whether the modal apparatus of $\mathbf{TTT}$ extends to it.

6.6 Cubical comparison

6.7 An alternative axiomatic approach

Rather than seeking a syntactic-by-construction proof, one can take Theorem 22 as a model and postulate a version of directed univalence at each layer. Concretely:

1. Add to $\mathbf{TTT}$ a constant ${\mathsf{dua}}_{\mathsf{Rezk}}:{\prod }_{A,B:{\mathcal{S}}_{\mathsf{Rezk}}}\mathsf{Fun}(A,B)\to {\mathsf{Hom}}_{{\mathcal{S}}_{\mathsf{Rezk}}}(A,B)$.

2. Add an axiom that ${\mathsf{dua}}_{\mathsf{Rezk}}$ is an equivalence.

3. Verify in standard models (bisimplicial sets, marked simplicial sets, $\infty$-toposes) that the postulated principle is sound.

This is the directed analogue of taking Voevodsky’s univalence as an axiom rather than deriving it from cubical methods. It establishes consistency with prevailing semantic models but leaves the syntactic story incomplete.

6.8 Summary table

7 Connections to $(\infty ,1)$-Natural Number Objects and HITs

7.1 Natural number objects in directed type theory

In ordinary HoTT, the natural numbers $\mathbb{N}$ are characterised by an initiality universal property: $(\mathbb{N},0,\mathsf{succ})$ is initial in the type of pointed endo-types. This characterisation generalises directly to the discrete sub-universe of $\mathbf{TTT}$: $\mathbb{N}$ is a type in $\mathcal{S}$ and is initial.

7.2 Higher inductive types and directed univalence

A higher inductive type (HIT) like $S^1$ has constructors and path constructors producing identifications. In the directed setting one wants directed-path constructors: a type with constructors and prescribed hom-types, defined synthetically.

7.3 Synthetic representation theory

Directed univalence connects to representation theory through the slogan: representations are functors. A representation of a group $G$ on a vector space is a functor $BG\to \mathsf{Vect}$, where $BG$ is the classifying type of $G$. In a hypothetical full directed type theory:

7.4 Synthetic adjunctions and Kan extensions

Directed univalence enables a direct treatment of adjunctions in synthetic $(\infty ,1)$-category theory. In the GWB setting, an adjunction $F⊣G:A\to B$ between objects of the directed universe of Rezk types becomes a single piece of data in ${\mathcal{S}}_{\mathsf{Rezk}}$:

7.5 Stability under base change

A subtle but important property of complete directed univalence is its behaviour under base change. If $f:C\to D$ is a directed morphism in ${\mathcal{S}}_{\mathsf{Rezk}}$, the induced functor $f^{\ast }:{\mathcal{S}}_{\mathsf{Rezk}}/D\to {\mathcal{S}}_{\mathsf{Rezk}}/C$ should preserve directed-univalent structure.

7.6 Comparison to formalisations: Coq-HoTT, Lean-mathlib, Cubical Agda, rzk

• Coq-HoTT and Lean-mathlib formalise symmetric univalence as a postulate.

• Cubical Agda makes symmetric univalence computational.

• The experimental proof assistant rzk  implements $\mathbf{STT}$ with topes and extension types; it does not yet implement triangulated modalities or prove directed univalence.

8 Discussion

8.1 Why is directed univalence so hard?

We can summarise the difficulty in three points.

1. Asymmetry of hom. The hom-type ${\mathsf{Hom}}_A(a,b)$ is asymmetric in $(a,b)$, while the identity type $a{=}_{A}b$ is symmetric. Many path-induction-based arguments fail directly.

2. Modal dependence. Even the discrete fragment requires modalities to mediate between symmetric and directed worlds. Non-discrete fragments will likely need richer modal apparatus.

3. Size issue. The universe is a large object. A directed structure on it would package its $(\infty ,1)$-categorical morphisms internally — a strictly stronger demand than packaging $\infty$-groupoidal equivalences.

8.2 What would change if Candidate III were proven?

1. Synthetic $(\infty ,1)$-category theory in $\mathbf{STT}$/$\mathbf{TTT}$ would gain a universe-theoretic foundation, not just a Yoneda-based one.

2. Functors $A\to B$ between Rezk types would automatically be morphisms in a Rezk universe, enabling direct manipulation of categories of categories.

3. Adjunctions would internalise: an adjunction $F⊣G$ would correspond to a single object in $\mathsf{Adj}({\mathcal{S}}_{\mathsf{Rezk}})$, accessible through directed transport.

4. Formalisation in a directed proof assistant (extension of rzk) would become tractable.

8.3 What would change if Candidate IV were proven?

Candidate IV is qualitatively stronger. If proven (likely in a 2-level theory):

1. The universe itself would be both an $\infty$-groupoid and an $(\infty ,1)$-category — with the structures coherently related.

2. Univalence and directed univalence would be compatible.

3. Higher directed univalence (for $(\infty ,n)$-categories) could be tackled inductively.

8.4 Limitations of this paper

This paper is expository and programmatic. We do not prove a new directed univalence theorem. The accompanying Haskell and Lean code formalise the discrete fragment of $\mathbf{TTT}$ in a toy model (Haskell) and as a postulate-based sketch (Lean), and exhibit the algebraic content. We hope these provide a productive substrate for future work.

9 Open Problems

We list four explicit open problems.

10 Conclusion

Directed univalence has come a long way since Riehl–Shulman 2017. Their original framework gave us simplicial type theory with an internalised hom-type and a partial straightening theorem for covariant fibrations. Gratzer–Weinberger–Buchholtz 2024 introduced the modal apparatus needed to internalise directed structure on the universe, and proved the first complete directed univalence theorem for the universe of discrete types.

The complete principle remains a research target. The path forward is layered: extend the modality structure to capture Segal-ness and Rezk-ness, prove successively stronger directed univalence statements at each layer, and ultimately reach a 2-level account where the universe carries both directed and undirected structure coherently. The reward, if it can be obtained, is a synthetic foundation for $(\infty ,1)$-category theory in which functors are directed morphisms in the universe — an ipso facto foundation for synthetic representation theory and beyond.

We close with a final observation. The classical univalence axiom internalised the slogan “isomorphic objects are equal”. A complete directed univalence axiom would internalise the slogan “functors are arrows in the universe of categories”. These are both deeply structuralist principles. The latter, if it can be proved, would unify the structuralist viewpoints of Lawvere, Awodey, and Voevodsky into a single foundational system in which the universe is itself a category.

Acknowledgments

This is a derivative exposition; original results are due to Emily Riehl, Michael Shulman, Daniel Gratzer, Jonathan Weinberger, and Ulrik Buchholtz. We thank these authors for the foundational work surveyed here.