# 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

A discussion of categorical semantics of homotopy type theory in a type-theoretic model category appears around def. 2.5 of

An exposition is in

Similar conisderations (using the term “typos” for something similar to a type-theoretic model category) are presented in

• André Joyal, What is categorical type theory, various talks in 2013, (pdf)

Revised on September 24, 2013 12:22:38 by Urs Schreiber (158.109.1.23)