`{!IsSurjInj F, !IsSurjInj (G o F)} : IsSurjInj G. Proof. constructor. - apply cancelR_isesssurj. - intros x y f. pose (p := (esssurj F x).2). pose (q := (esssurj F y).2). cbn in *. refine (p^$ $@ _ $@ q). apply (fmap F). apply (essinj (G o F)). refine (_ $@ f $@ _). + exact (fmap G p). + exact (fmap G q^$). Defined.
Require Import Basics.Overture Basics.Tactics Basics.Iff. Require Import WildCat.Core. Require Import WildCat.NatTrans. Require Import WildCat.Sigma.