Definition is_z_iso_co_eilenberg_moore {x y : co_eilenberg_moore_cat} (f : x --> y) (Hf : is_z_isomorphism (pr11 f)) : is_z_isomorphism f. Proof. pose (H := make_z_iso _ _ Hf). use make_is_z_isomorphism. - use make_mor_co_eilenberg_moore. + exact (inv_from_z_iso H). + apply (is_z_iso_disp_dialgebra _ _ Hf (pr21 f)). - split. + abstract (use eq_mor_co_eilenberg_moore ; cbn ; apply (z_iso_inv_after_z_iso H)). + abstract (use eq_mor_co_eilenberg_moore ; cbn ; apply (z_iso_after_z_iso_inv H)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Categories.Dialgebras. Require Import UniMath.CategoryTheory.Subcategory.Core. Require Import UniMath.CategoryTheory.Subcategory.Full. Require Import UniMath.CategoryTheory.Monads.Comonads.