left universal property of equality

eq_univ.v

Require Import Overture Equivalences.

Goal forall A (a : A) (B : forall x, a = x -> Type) (x : A), Equiv (forall x (p : a = x), B x p) (B a (idpath a)).
Proof.
  intros.
  apply (equiv_adjointify
           (fun f => f _ idpath)
           (fun p0 => fun x0 p => match p as p' in (_ = y) return B y p' with
                                    | idpath => p0
                                  end)).
  - intro. reflexivity.
  - intro.