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.
