fact: Definition dcate_moveR_Ve {A} {D : A -> Type} `{DHasEquivs A D} {a b c : A} {e : b $<~> a} {f : b $<~> c} {g : c $<~> a} {p : cate_fun e $== g $o f} {a' : D a} {b' : D b} {c' : D c} (e' : DCatEquiv e b' a') (f' : DCatEquiv f b' c') (g' : DCatEquiv g c' a') (p' : DGpdHom p (dcate_fun e') (dcate_fun g' $o' f')) : DGpdHom (cate_moveR_Ve e f g p) (dcate_fun g'^-1$' $o' e') (dcate_fun f').
imports: Basics.Overture Basics.Tactics Basics.Equivalences Types.Sigma WildCat.Core WildCat.Displayed WildCat.Equiv