fact: Definition dcat_precomp {A : Type} {D : A -> Type} `{IsD01Cat A D} {a b c : A} {f : a $-> b} {a' : D a} {b' : D b} {c' : D c} (f' : DHom f a' b') : forall (g : b $-> c), DHom g b' c' -> DHom (g $o f) a' c' := fun _ g' => g' $o' f'.
imports: Basics.Overture Basics.PathGroupoids Basics.Tactics Types.Sigma WildCat.Core WildCat.Prod