{A} {D : A -> Type} `{DHasEquivs A D} {a b c : A} {f : c $<~> b} {g : a $-> b} {a' : D a} {b' : D b} {c' : D c} (f' : DCatEquiv f c' b') (g' : DHom g a' b') : DGpdHom (compose_h_Vh f g) (dcate_fun f' $o' (dcate_fun f'^-1$' $o' g')) g' := (dcat_assoc_opp _ _ _) $@' (dcate_isretr f' $@R' g') $@' dcat_idl g'.
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.