Having some more random thoughts about how some parts directed
homotopy type theory might look. I don't think I have the semantics
chops to really prove soundness of any of these axioms, but it's fun
to think about. Here's a brain dump:

Start with the observation that we have
(A : type) (P : A → type) (e : A) → ((x : A) → e ≡ x → P x) ≡ P e

this equivalence is (part of) an inductive definition of ≡ as a
positive type. We say what happens when we have a function from x ≡ e
into some other A-indexed type P x: you just substitute the e for the
argument of P. This is just like how + breaks apart when sent into
some other type:

(A B : type) (P : type) → ((A + B) → P) ≡ (A → P) × (B → P)

Ok, great, now I'm going to imagine that the type theory has a notion
of a covariant type family indexed over A, write it as P : A →+
type. This is a refinement of A → type that behaves like a covariant
functor: for any a ≤ b ∈ A, there will be a function P a → P b.

In that case, I want to make a sort of inductive definition of ≤, the
internalization of the directed hom. So I say:

(A : type) (P : A →+ type) (e : A) → ((x : A) → e ≤ x → P x) ≡ P e

I can view this as defining ≤ if I know what it means to be a
covariant type family, or I can view it as defining what a covariant
type family is assuming I know what ≤ means. Let me take up the latter
perspective for a moment, and ask what a covariant functor is between
arbitrary types A and B. I can't just say that

P is A →+ B iff it's a function A → B such that
(e : A) → ((x : A) → e ≤ x → P x) ≡ P e

because the thing on the left of the ≡ wants to be a type, while the
thing on the right is of type B. I want some kind of Pi-ish operator
that "quantifies" over elements of A and gives me back an element of
B. Well when I do logic in lattices, forall is an infimum, so let me
write, suggestively:

P is A →+ B iff it's a function A → B such that
(e : A) → inf_{x ≥ e} P x ≡ P e

Well what kind of universal property would the infimum satisfy? Hmmm.
It's that anything less than the infimum is less than everything it's
infimumming over:

(t ≤ (inf_{x ≥ e} P x)) ≡ (x : A) → x ≥ e → t ≤ P x

but by asserting that P e is equal to the infimum, I might as well say
that it has this UMP! So here's another attempted definition of
covariance:

P is A →+ B iff it's a function A → B such that
(e : A) (t : B) →
   (t ≤ P e) ≡ ((x : A) → x ≥ e → t ≤ P x)

And actually, in order to be covariant in higher-dimensional morphisms
as well, I think I want that rightmost arrow to be a covariant
arrow as well. This seems like a bit of nasty recursiveness. But I can
sweep it under the rug by asserting a univalence-like principle, that
≤ on types is the same thing as covariant functions:

(A ≤ B) ≡ (Σ (A → B) covariant)

and defining

covariant : {A B : Set} (A → B) → Set
covariant P = (e : A) (t : B) →
   (t ≤ P e) ≡ ((x : A) → (e ≤ x) ≤ (t ≤ P x))

and then I think I want to assert that ≤ itself is covariant in its
second argument:

≤cov : {A : Set} (x : A) → covariant {A} {Set} (λ y → x ≤ y)

and I think from this you can get reflexivity and transitivity of ≤,
and covariance of the identity function, and I think you really
ought to be able to derive that ≤ is contravariant in its first
argument but I still haven't agda'ed it up so don't believe me yet.

What's dependent covariance, then? Suppose I have a contravariant
B : A →- Set. Then I should get transport from a1 ≤ a2 to B a2 →+ B a1.
So something like the following?

dep-covariant : {A : Set} {B : A →+ Set} ((x : A) → B x) → Set
dep-covariant P = (e : A) (t : B e) →
   (t ≤ P e) ≡ ((x : A) (q : e ≤ x) → (transport B q t ≤ P x))

I'm definitely not sure I'm getting all the co-s and contra-s right.