{A} {D : A -> Type} `{IsD1Cat A D} {b c : A} {f : b $-> c} {mon : Monic f} {b' : D b} {c' : D c} (f' : DHom f b' c') := forall (a : A) (g h : a $-> b) (p : f $o g $== f $o h) (a' : D a) (g' : DHom g a' b') (h' : DHom h a' b'), DGpdHom p (f' $o' g') (f' $o' h') -> DGpdHom (mon a g h p) g' h'.
Require Import Basics.Overture. Require Import Basics.PathGroupoids. Require Import Basics.Tactics. Require Import Types.Sigma. Require Import WildCat.Core. Require Import WildCat.Prod.