{A : Type} {D : A -> Type} `{IsD0Gpd A D} {a b c : A} {f : a $== b} {g : b $== c} {a' : D a} {b' : D b} {c' : D c} : DGpdHom f a' b' -> DGpdHom g b' c' -> DGpdHom (g $o f) a' c' := fun f' g' => g' $o' f'.
Require Import Basics.Overture. Require Import Basics.PathGroupoids. Require Import Basics.Tactics. Require Import Types.Sigma. Require Import WildCat.Core. Require Import WildCat.Prod.