# Contents

## Idea

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

One candidate for full omega-categories i.e. (∞,∞)-categories is opetopic type theory.

## References

Also chapters 7 and 8 of

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

• Andreas Nuyts?, Towards a Directed Homotopy Type Theory based on 4 Kinds of Variance, PDF

Revised on January 22, 2016 16:55:15 by Bas Spitters (93.160.112.96)