{A} {D : A -> Type} `{DHasEquivs A D} {a b c d : A} {f : a $<~> b} {g : b $<~> c} {h : c $<~> d} {a'} {b'} {c'} {d'} (f' : DCatEquiv f a' b') (g' : DCatEquiv g b' c') (h' : DCatEquiv h c' d') : DGpdHom (compose_cate_assoc f g h) (dcate_fun ((h' $oE' g') $oE' f')) (dcate_fun (h' $oE' (g' $oE' f'))). Proof. refine (dcompose_cate_fun _ f' $@' _ $@' dcat_assoc (dcate_fun f') g' h' $@' _ $@' dcompose_cate_funinv h' _). - apply (dcompose_cate_fun h' g' $@R' _). - apply (_ $@L' dcompose_cate_funinv g' f'). 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.