demap_compose' {A B : Type} {DA : A -> Type} `{DHasEquivs A DA} {DB : B -> Type} `{DHasEquivs B DB} (F : A -> B) `{!Is0Functor F, !Is1Functor F} (F' : forall (a : A), DA a -> DB (F a)) `{!IsD0Functor F F', !IsD1Functor F F'} {a b c : A} {f : a $<~> b} {g : b $<~> c} {a' : DA a} {b' : DA b} {c' : DA c} (f' : DCatEquiv f a' b') (g' : DCatEquiv g b' c') : DGpdHom (emap_compose' F f g) (dcate_fun (demap F F' (g' $oE' f'))) (dcate_fun ((demap F F' g') $oE' (demap F F' f'))). Proof. refine (demap_compose F F' f' g' $@' _). apply dgpd_rev. refine (dcompose_cate_fun _ _ $@' _). exact (dcate_buildequiv_fun _ $@@' 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.