{A} {D : A -> Type} `{DHasEquivs A D} {a b c : A} {e : a $<~> b} {f : b $<~> c} {a' : D a} {b' : D b} {c' : D c} (e' : DCatEquiv e a' b') (f' : DCatEquiv f b' c') : DGpdHom (cate_inv_compose e f) (dcate_fun (f' $oE' e')^-1$') (dcate_fun (e'^-1$' $oE' f'^-1$')). Proof. refine (_ $@' (dcompose_cate_fun e'^-1$' f'^-1$')^$'). - snrapply dcate_inv_adjointify. - exact isd0gpd_hom. 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.