proposition: Lemma hom_isoK (c : C) (d : D) (f : {hom F c, d}) : hom_inv (hom_iso f) = f.
proof: Proof. rewrite /hom_inv /hom_iso; apply hom_ext => /=. by rewrite functor_o -(natural_head (eps _)) triL. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures)