A preprint has appeared on the arXiv outlining a directed HoTT by Paige Randall North.Just from skimming so far it appears to be a standard Martin-Lof with a core, op and hom-type.The core type gives the set of objects of a type (I suppose types are now categories of sorts). The op type gives the opposite category, then the hom type is the directed path type.As far as I can tell this type theory has semantics in Cat.I would be interested on others thoughts on this.