proposition: Proposition IsMonic_HasRetraction {A} `{Is1Cat A} {b c : A} (f : b $-> c) : RetractionOf f -> Monic f.
proof: Proof. intros retraction a g h eq_fg_fh. destruct retraction as [left_inverse is_retraction]. apply (is0functor_postcomp _ _ _ left_inverse) in eq_fg_fh; unfold cat_postcomp in eq_fg_fh. rewrite <- 2 cat_assoc, is_retraction, 2 cat_idl in eq_fg_fh. assumption. Defined.
imports: HoTT(Basics.Overture Basics.Tactics) HoTT(Types.Forall) HoTT(WildCat.Core WildCat.Bifunctor WildCat.Prod WildCat.NatTrans WildCat.Equiv)