elegant Reedy category


Model category theory

model category



Universal constructions


Producing new model structures

Presentation of (,1)(\infty,1)-categories

Model structures

for \infty-groupoids

for ∞-groupoids

for nn-groupoids

for \infty-groups

for \infty-algebras



for stable/spectrum objects

for (,1)(\infty,1)-categories

for stable (,1)(\infty,1)-categories

for (,1)(\infty,1)-operads

for (n,r)(n,r)-categories

for (,1)(\infty,1)-sheaves / \infty-stacks

Homotopy theory




An elegant Reedy category is a Reedy category RR such that the following equivalent conditions hold

  • For every monomorphism ABA\hookrightarrow B of presheaves on RR and every xRx\in R, the induced map A x⨿ L xAL xBB xA_x \amalg_{L_x A} L_x B \to B_x is a monomorphism.

  • Every span of codegeneracy maps in R R_- has an absolute pushout in R R_-.

  • Both the following conditions hold:

    1. For every monomorphism ABA\hookrightarrow B of presheaves on RR, every nondegenerate element of AA remains nondegenerate in BB.

    2. Every element of a presheaf RR is a degeneracy of some nondegenerate element in a unique way.

In particular, if RR is elegant, then every codegeneracy map is a split epimorphism.


Model structures


If RR is an elegant Reedy category and MM is a model category in which the cofibrations are exactly the monomorphisms, then the Reedy model structure and the injective model structure on M R opM^{R^{op}} coincide.

In particular, this implies that every MM-valued presheaf on an elegant Reedy category is Reedy cofibrant.


  • The simplex category Δ\Delta is an elegant Reedy category.

  • Joyal’s disk categories Θ n\Theta_n are elegant Reedy categories.

  • Every direct category is a Reedy category with no degeneracies, hence trivially an elegant one.

  • If XX is any presheaf on an elegant Reedy category RR, then the opposite of its category of elements (elX) op(el X)^{op} is again an elegant Reedy category. This is fairly easy to see from the fact that Set elXSet^{el X} is equivalent to the slice category Set R op/XSet^{R^{op}}/X.

  • Every EZ-Reedy category? is elegant.

Note that unlike the notion of Reedy category, the notion of elegant Reedy category is not self-dual: if RR is elegant then R opR^{op} will not generally be elegant.


Elegant Reedy categories are useful to model homotopy type theory.

  • Mike Shulman, Univalence for inverse diagrams and homotopy canonicity arXiv:1203.3253

  • Benno van den Berg and Ieke Moerdijk, W-types in homotopy type theory, PDF

Revised on February 1, 2014 10:03:31 by Bas Spitters (