{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) {ff : forall a, Is0Functor (F a)} : SplEssSurj (fun (x:sig B) => (x.1 ; F x.1 x.2)) <-> (forall a, SplEssSurj (F a)). Proof. split. - intros fs a c. pose (s := fs (a;c)). destruct s as [[a' b] [p q]]; cbn in *. destruct p; cbn in q. exists b. exact q. - intros fs [a c]. exists (a ; (esssurj (F a) c).1); cbn. exists idpath; cbn. exact ((esssurj (F a) c).2). Defined.
Require Import Basics.Overture Basics.Tactics Basics.Iff. Require Import WildCat.Core. Require Import WildCat.NatTrans. Require Import WildCat.Sigma.