fact: Definition transport_hom (a a' b b' : C) (pa : a = a') (pb : b = b') (f : {hom a, b}) : {hom a', b'} := eq_rect b (fun y => {hom a', y}) (eq_rect a (fun x => {hom x, b}) f a' pa) b' pb.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures)