---
title: "The homotopy types of directed path and trace spaces"
authors:
  - "Philippe Gaucher"
year: 2026
venue: "arXiv:math.AT"
arxiv: "2609.11454"
doi: null
source: "https://arxiv.org/abs/2609.11454"
topics:
  - "curiosity"
  - "maths-foundations"
  - "algebraic-topology"
  - "directed-homotopy"
seed_rank: 1832
seed_batch: "curiosity-2026-09-15"
reviewed: "2026-09-15"
pool: "maths-foundations"
relevance_score: 9
lineage: directed-homotopy
cites:
  - title: "The homotopy types of directed path and trace spaces"
    url: "https://arxiv.org/abs/2609.11454"
    year: 2026
    arxiv: "2609.11454"
    doi: null
see:
  - "1452-directed-univalence-for-simplicial-objects-in-an-infinity-topos"
---

# The homotopy types of directed path and trace spaces

## One-sentence takeaway

A saturated directed space can have trace space homeomorphic to a square while the directed path space has nontrivial π₁ — so the canonical quotient is not a weak homotopy equivalence.

## Why it's lovely

Why you might love this: directed homotopy quietly assumes path spaces and trace spaces are 'the same up to homotopy.' Here they are not: traces look like a square, directed paths carry a loop. A sharp counterexample that anyone writing concurrent or directed type theory should keep in a pocket.

## Key ideas

- Constructs a saturated d-space with Hausdorff Δ-generated carrier.
- Trace space between two points ≅ square; directed path space has nontrivial fundamental group.
- Canonical quotient path→trace fails to be a weak homotopy equivalence.
- Separates two models often treated interchangeably in directed algebraic topology.

## Caveats

Existence/counterexample paper; does not give a classification of when path≃trace. Pair with directed-univalence card 1452 for Broadside's directed shelf, not as a citation of the same result.

## Links

- arXiv abs: https://arxiv.org/abs/2609.11454
- PDF: https://arxiv.org/pdf/2609.11454.pdf