{A} {D : A -> Type} `{DHasEquivs A D} {a b : A} {f : a $<~> b} {a' : D a} {b' : D b} (f' : DCatEquiv f a' b') : DGpdHom (compose_cate_idr f) (dcate_fun (f' $oE' did_cate a')) (dcate_fun f'). Proof. refine (dcompose_cate_fun f' _ $@' _ $@' dcat_idr (dcate_fun f')). rapply (_ $@L' dcate_buildequiv_fun _). 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.