{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)). Proof. constructor. - apply isesssurj_iff_sigma; exact _. - intros [a1 b1] [a2 b2] [p f]; cbn in *. destruct p; cbn in *. exists idpath; cbn. exact (essinj (F a1) f). Defined.
Require Import Basics.Overture Basics.Tactics Basics.Iff. Require Import WildCat.Core. Require Import WildCat.NatTrans. Require Import WildCat.Sigma.