proposition: Lemma initials_unique' (x x': X) `{Initial x} `{Initial x'}: iso_arrows (initial_arrow x': x ⟶ x') (initial_arrow x).
proof: Proof. Proof with reflexivity. split. rewrite <- (H4 _ cat_id), <- H4... rewrite <- (H2 _ cat_id), <- H2... Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.theory.setoids MathClasses.interfaces.functors MathClasses.theory.jections