proposition: Lemma sections_are_monic : Section f → Monic f.
proof: Proof. autounfold. intros. destruct X. constructor; intros. rewrite <- id_left. symmetry. rewrite <- id_left. transitivity ((section0 ∘ f) ∘ g2); [ now apply compose_respects |]; transitivity ((section0 ∘ f) ∘ g1); [| now apply compose_respects ]. reassociate_left. Qed.
imports: Category.Lib Category.Theory.Category