proposition: Lemma hom_invK (c : C) (d : D) (g : {hom c, G d}) : hom_iso (hom_inv g) = g.
proof: Proof. rewrite /hom_inv /hom_iso; apply hom_ext => /=. by rewrite functor_o hom_compA (natural (eta A)) -hom_compA triR. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures)