{A B : Type} {F : A -> B} {G : A -> B} `{IsSurjInj A B F} `{!Is0Functor G} (alpha : G $=> F) : IsSurjInj G. Proof. constructor. - apply (isesssurj_transf alpha). - intros x y f. apply (essinj F). refine (_ $@ f $@ _). + symmetry; apply alpha. + apply alpha. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Iff. Require Import WildCat.Core. Require Import WildCat.NatTrans. Require Import WildCat.Sigma.