{A} {D : A -> Type} `{IsD1Cat A D} {a b : A} {f : a $-> b} {epi : Epic f} {a' : D a} {b' : D b} (f' : DHom f a' b') := forall (c : A) (g h : b $-> c) (p : g $o f $== h $o f) (c' : D c) (g' : DHom g b' c') (h' : DHom h b' c'), DGpdHom p (g' $o' f') (h' $o' f') -> DGpdHom (epi c g h p) g' h'. Global Instance isgraph_total {A : Type} (D : A -> Type) `{IsDGraph A D} : IsGraph (sig D). Proof. srapply Build_IsGraph. intros [a a'] [b b']. exact {f : a $-> b & DHom f a' b'}. Defined.
Require Import Basics.Overture. Require Import Basics.PathGroupoids. Require Import Basics.Tactics. Require Import Types.Sigma. Require Import WildCat.Core. Require Import WildCat.Prod.