proposition: Proposition IsEpic_HasSection {A} `{Is1Cat A} {a b : A} (f : a $-> b) : SectionOf f -> Epic f.
proof: Proof. intros section c g h eq_gf_hf. destruct section as [right_inverse is_section]. apply (is0functor_precomp _ _ _ right_inverse) in eq_gf_hf; unfold cat_precomp in eq_gf_hf. rewrite 2 cat_assoc, is_section, 2 cat_idr in eq_gf_hf. exact eq_gf_hf. Defined.
imports: HoTT(Basics.Overture Basics.Tactics) HoTT(Types.Forall) HoTT(WildCat.Core WildCat.Bifunctor WildCat.Prod WildCat.NatTrans WildCat.Equiv)