fact: Definition issurjinj_sigma {A : Type} (B C : A -> Type) `{forall a, IsGraph (B a)} `{forall a, Is01Cat (B a)} `{forall a, Is0Gpd (B a)} `{forall a, IsGraph (C a)} `{forall a, Is01Cat (C a)} `{forall a, Is0Gpd (C a)} (F : forall a, B a -> C a) `{forall a, Is0Functor (F a)} `{forall a, IsSurjInj (F a)} : IsSurjInj (fun (x:sig B) => (x.1 ; F x.1 x.2)).
imports: Basics.Overture Basics.Tactics WildCat.Core WildCat.NatTrans WildCat.Sigma