Lemma μ_1_identity : μ_1 = identity `T . Proof. apply pathsinv0. apply fbracket_unique. split. - apply nat_trans_eq_alt. intros; simpl. rewrite id_right. apply idpath. - apply nat_trans_eq_alt. intro c. simpl. rewrite id_right. assert (H':= θ_Strength1_int_implies_θ_Strength1 _ θ_strength1_int). red in H'. simpl in H'. assert (H2 := H' (`T)). assert (H3 := nat_trans_eq_pointwise H2 c). simpl in *. intermediate_path (identity _ · pr1 (τ T) c). + apply cancel_postcomposition. apply H3. + apply id_left. 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.SimplifiedHSS.SubstitutionSystems. Require Import UniMath.SubstitutionSystems.Notation.