just proved it this morning was

{A : Set} {a b : A} → (a ≡ b) ≡ ((c : A) → b ≡ c → a ≡ c)

Here's why: it's pretty easy to see that both

(a ≡ b) ← ((c : A) → b ≡ c → a ≡ c)

and

(a ≡ b) → ((c : A) → b ≡ c → a ≡ c)

because for the first one, you just use reflexivity of ≡ (after

choosing c to be b) and for the second, you use transitivity.

What surprised me was that these maps are actually inverse to each

other. This means that essentially the

*only*way you can prove

(c : A) → b ≡ c → a ≡ c

is by already having a ≡ b in your pocket and composing it with the

b ≡ c.

So I guess this is another consequence of the intrinsic

naturality/parametricity/fibrationiness of the dependent function

space in hott.

Here's the actual proof:

into : {A : Set} {a b : A} → (a ≡ b) → ((c : A) → b ≡ c → a ≡ c) into refl = λ x → id _ outo : {A : Set} {a b : A} → ((c : A) → b ≡ c → a ≡ c) → (a ≡ b) outo f = f _ refl into-outo : {A : Set} {a b : A} → (g : a ≡ b) → outo (into g) ≡ g into-outo refl = refl outo-into : {A : Set} {a b : A} → (f : ((c : A) → (b ≡ c) → (a ≡ c))) → into (outo f) ≡ f outo-into f = funext (λ x → funext (λ y → lemma1 (f _ refl) y ∘ lemma2 refl y f)) where lemma1 : {A : Set} {a b c : A} (g : a ≡ b) (h : b ≡ c) → into g _ h ≡ g ∘ h lemma1 refl h = refl lemma2 : {A : Set} {a b c d : A} (p : b ≡ c) (q : c ≡ d) (f : (c : A) → b ≡ c → a ≡ c) → (f _ p) ∘ q ≡ f _ (p ∘ q) lemma2 refl refl f = refl-right-unit _ result : {A : Set} {a b : A} → (a ≡ b) ≡ ((c : A) → b ≡ c → a ≡ c) result = iso-to-path into outo outo-into into-outo

A thing I'd like to know is if michael warren's definition of the directed

hom --- let me write it as a ≤ b --- satisfies

(a ≤ b) ≡ ((c : A) → b ≤ c → a ≤ c)

because this while this equivalence also

*implies*reflexivity and transitivity

of ≤, it seems compatible with ≤ not being symmetric.