Definition SigmaMonoid_compatibility (X : total_category SigmaMonoid_disp_cat_no_compatibility) : UU. Proof. set (x := pr1 X). set (η := monoid_data_unit _ (pr22 X : monoid _ _)). set (μ := monoid_data_multiplication _ (pr22 X : monoid _ _)). set (τ := pr12 X : H x --> x). set (st := pr1 θ (x ,, η) x). exact (SigmaMonoid_characteristic_equation x η μ τ st). 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.