proposition: Lemma transport_homF (a a' b b' : C) (pa : a = a') (pb : b = b') (f : {hom a, b}) : transport_hom pa pb f = [hom hom_of_eq pb \o f \o hom_of_eq (esym pa)].
proof: Proof. apply hom_ext; by subst a' b'. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures)