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.