Lemma disp_Monad_laws_from_hss : disp_Monad_laws disp_Monad_data_from_hss. Proof. split. - unfold disp_Monad_data_from_hss; simpl; split. + apply Monad_law_1_from_hss. + apply Monad_law_2_from_hss. - unfold disp_Monad_data_from_hss; simpl. intro c. intermediate_path (pr1 μ_3 c). + set (H1 := μ_3_T_μ_2_μ_2). set (H2 := nat_trans_eq_weq (homset_property C) _ _ H1). apply pathsinv0, H2. + set (H1 := μ_3_μ_2_T_μ_2). set (H2 := nat_trans_eq_weq (homset_property C) _ _ H1). apply pathsinv0, H2. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.PointedFunctorsComposition. Require Import UniMath.CategoryTheory.BicatOfCatsElementary. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.SubstitutionSystems.SubstitutionSystems. Require Import UniMath.SubstitutionSystems.Notation.