Inverse Diagrams and Reedy Fibrancy

Definition

An inverse category is a category where the relation $x<y⟺\exists f:x\to y,x\ne y$ is well-founded. Diagrams over these categories (e.g., towers $A_0\leftarrow A_1\leftarrow \dots$) contain no infinite loops.

Reedy Fibrancy

A condition on diagrams ensuring that homotopy limits coincide with strict limits. For inverse categories, Reedy fibrancy can often be constructed strictly. This allows one to define complex coherent structures without the full machinery of $(\infty ,1)$-categories, by building them up level by level.

References

• Shulman, M. (2015). “Univalence for inverse diagrams and homotopy canonicity”. Mathematical Structures in Computer Science.