Definition make_symmetric_monoidal_comonad {T : Comonad C} {Tm : fmonoidal_lax M M (pr1 T)} (Ts : is_symmetric_monoidal_functor HM HM Tm) (Hδ : is_mon_nat_trans Tm (comp_fmonoidal_lax Tm Tm) (δ T)) (Hε : is_mon_nat_trans Tm (identity_fmonoidal_lax M) (ε T)) : symmetric_monoidal_comonad. Proof. use tpair. - use tpair. + exact (pr1 T). + exact (Tm,,Ts). - use tpair. + exact (pr2 T). + exact (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.