fact: Definition DGpdHom {A : Type} {D : A -> Type} `{IsD0Gpd A D} {a b : A} (f : a $== b) (a' : D a) (b' : D b) := DHom f a' b'.
imports: Basics.Overture Basics.PathGroupoids Basics.Tactics Types.Sigma WildCat.Core WildCat.Prod