# Contents

## Idea

What homotopy type theory is for homotopy theory/(∞,1)-category theory, directed homotopy type theory is for directed homotopy theory/(∞,n)-category theory.

## References

Also chapters 7 and 8 fo

• Dan Licata, Dependently Typed Programming with Domain-Specific Logics PhD thesis, (pdf)

Revised on September 26, 2013 16:21:10 by Urs Schreiber (158.109.1.23)