{A} {D : A -> Type} `{DHasEquivs A D} {a b : A} (p : a = b) (a' : D a) (b' : D b) : transport D p a' = b' -> DCatEquiv (cat_equiv_path a b p) a' b'. Proof. intro p'. destruct p, p'. reflexivity. Defined.
Require Import Basics.Overture. Require Import Basics.Tactics. Require Import Basics.Equivalences. Require Import Types.Sigma. Require Import WildCat.Core. Require Import WildCat.Displayed. Require Import WildCat.Equiv.