{A} {D : A -> Type} `{DHasEquivs A D} {a b c : A} {e : b $<~> a} {f : a $-> c} {g : b $-> c} {p : f $== g $o e^-1$} {a' : D a} {b' : D b} {c' : D c} (e' : DCatEquiv e b' a') (f' : DHom f a' c') (g' : DHom g b' c') (p' : DGpdHom p f' (g' $o' e'^-1$')) : DGpdHom (cate_moveR_eM e f g p) (f' $o' e') g'. Proof. apply (dcate_epic_equiv e'^-1$'). exact (dcompose_hh_V _ _ $@' p'). 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.