Definition disp_cat_symmetric_monoidal_comonads : disp_cat (category_symmetric_lax_monoidal_functors HM HM). Proof. use disp_struct. - intros [F [Fm Fs]]. use total2. + exact (comonads_category_disp F). + intro H. induction H as [[δ ε] _]. exact (symmetric_monoidal_comonads_extra_laws Fm δ ε). - intros F G T T' α. exact (disp_Comonad_Mor_laws (pr11 T) (pr11 T') (pr1 α)). - intros. apply isaprop_disp_Comonad_Mor_laws. - intros F T. apply comonads_category_id_subproof. exact (pr21 T). - intros F F' F'' T T' T'' α α' Hα Hα'. cbn in *. exact (comonads_category_comp_subproof (pr11 T) (pr21 T) (pr11 T') (pr21 T') (pr11 T'') (pr21 T'') _ _ Hα 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.FunctorCategory. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Functors. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Sigma. Require Import UniMath.CategoryTheory.DisplayedCats.SIP. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Monads.Comonads.