{A B : Type} {F : A -> B} {G : A -> B} `{SplEssSurj A B F} `{!Is0Functor G} (alpha : G $=> F) : SplEssSurj G. Proof. intros b. exists ((esssurj F b).1). refine (_ $@ (esssurj F b).2). apply alpha. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Iff. Require Import WildCat.Core. Require Import WildCat.NatTrans. Require Import WildCat.Sigma.