fact: Definition did_cate_fun {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 _.
imports: Basics.Overture Basics.Tactics Basics.Equivalences Types.Sigma WildCat.Core WildCat.Displayed WildCat.Equiv