Definition mhss_to_sigma_monoid (t : mhss Mon_V H θ) : SigmaMonoid θ. Proof. exists (pr1 t). exists (tau_from_alg Mon_V H θ t ,, mhss_monoid Mon_V H θ t). exact (mfbracket_τ Mon_V H θ t (Z := (pr1 t,, μ_0 Mon_V H θ t)) (identity _)). 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.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Sigma. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Actegories.MorphismsOfActegories. Require Import UniMath.CategoryTheory.Monoidal.CategoriesOfMonoids. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.SubstitutionSystems.GeneralizedSubstitutionSystems. Import BifunctorNotations.