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