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