Definition postcomp_with_equalizer_mor (a : ob C) (j : a --> E) : ∑ (k : a --> c), (k · f = k · g). Proof. exists (j · h). refine (!assoc _ _ _ @ _). refine (_ @ assoc _ _ _). apply maponpaths. assumption. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Retracts.