proposition: Lemma natural : naturality F G f.
proof: Proof. move=> a b h. rewrite /f !transport_codomF 2!homcompE 2!compfid. have /hom_ext -> : [hom (hom_of_eq (Iobj b) \o F # h)] = [hom tc (F # h)] by rewrite transport_codomF. by rewrite Imor transport_domF homfunK /= esymK. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures)