---
title: "(2-dep,$Σ$)-categories are not generalised categories with families"
authors:
  - "Luis Gambarte"
year: 2026
venue: "arXiv:math.CT"
arxiv: "2609.01869"
doi: null
source: "https://arxiv.org/abs/2609.01869"
topics:
  - "curiosity"
  - "maths-foundations"
seed_rank: 1647
seed_batch: "curiosity-2026-09-09"
reviewed: "2026-09-09"
pool: "maths-foundations"
relevance_score: 10
lineage: dependent-type-foundations
cites:
  - title: "(2-dep,$Σ$)-categories are not generalised categories with families"
    url: "https://arxiv.org/abs/2609.01869"
    year: 2026
    arxiv: "2609.01869"
    doi: null
see:
  - "1586-on-left-adjoints-preserving-colimits-in-homotopy-type-theory"
---

# (2-dep,$Σ$)-categories are not generalised categories with families

## One-sentence takeaway

(2-dep, Σ)-categories — a natural 2-dimensional dependent-type doctrine — are not generalised categories with families.

## Why it's lovely

Why you might love this: the zoo of "categorical dependent type theory" doctrines keeps growing (CwF, comprehension categories, natural models, generalised CwF…). Gambarte shows a clean 2-dimensional candidate sits outside the generalised-CwF biequivalence class. Negative results that redraw the map of the zoo are peak curiosity.

## Key ideas

- Generalised CwF (Coraglia–Emmenegger) biequivalent to comprehension categories.
- (2-dep, Σ)-categories as a 2-dimensional dependent-typing doctrine.
- They are not generalised CwF — the doctrines genuinely diverge.
- Useful boundary marker for anyone formalising dependent types categorically (ano / proof assistants).

## Caveats

Does not propose a "best" doctrine; only separates two candidates. Read as a map-correction, not a compiler recipe.

## Links

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