nLab directed homotopy type theory - contents

directed homotopy type theory

(directed enhancement of homotopy type theory with types behaving like $(\infty,n)$-categories)

• directed univalence

• simplicial homotopy type theory

  • hom type

  • Segal type

  • isomorphism in a Segal type

  • Rezk type

  • discrete Segal type

  • covariant type family

  • contravariant type family

• opetopic type theory