{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 : A} {a' : DA a} : DGpdHom (emap_id F) (dcate_fun (demap F F' (did_cate a'))) (dcate_fun (did_cate (F' a a'))). Proof. refine (dcate_buildequiv_fun _ $@' _). refine (dfmap2 F F' (did_cate_fun a') $@' _ $@' _). - rapply dfmap_id. - apply dgpd_rev. exact (did_cate_fun (F' a a')). 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.