proposition: Lemma pairhom'_in_hom : inhom (pairhom' : el (a1, b1).1 + el (a1, b1).2 -> el (a2, b2).1 + el (a2, b2).2).
proof: Proof. rewrite /inhom /= /ProductCategory.inhom /=. set s := ProductCategory.separated _. have [/= s1 s2] : s by split => /= x; [exists (f x) | exists (g x)]. exists (conj s1 s2); split. - set h := ProductCategory.sepfst _. rewrite (_ : h = f); first exact: isHom_inhom. by rewrite boolp.funeqE => ?; rewrite /h /=; case: cid => ? []. - set h := ProductCategory.sepsnd _. rewrite (_ : h = g); first exact: isHom_inhom. by rewrite boolp.funeqE => ?; rewrite /h /=; case: cid => ? []. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib category HB(structures)