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