Definition ComonadCoalg_disp_id_comp {C : category} (T : Comonad C) : disp_cat_id_comp C (ComonadCoalg_disp_ob_mor T).
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.Monads.MonadAlgebras. Require Import UniMath.CategoryTheory.Monads.Comonads. Require Import UniMath.CategoryTheory.Monads.ComonadCoalgebras. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total.