{A} {D : A -> Type} `{DHasEquivs A D} {a : A} (a' : D a) : DGpdHom (id_cate_fun a) (dcate_fun (did_cate a')) (DId a') := dcate_buildequiv_fun _.
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.