# Type-theoretic model categories

under construction

## Idea

Homotopy type theory has categorical semantics in suitable categories which in turn present certain (infinity,1)-categories.

Decomposing the structure in homotopy type theory in layers as

1. dependent type theory

2. with identity types

3. and univalent universe types.

A 1-category whose internal logic can interpret this needs to

1. equipped with a weak factorization system with stable path objects, such that acyclic cofibrations are preserved by pullback along fibrations between fibrant objects.

2. (needs to be finished)

## References

Around def. 2.5 of

Revised on May 18, 2012 20:43:25 by Urs Schreiber (89.204.137.144)