proposition: Lemma μ_1_identity : μ_1 = identity `T .
proof: 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.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.PointedFunctors UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.HorizontalComposition UniMath.CategoryTheory.PointedFunctorsComposition UniMath.CategoryTheory.BicatOfCatsElementary UniMath.SubstitutionSystems.Signatures UniMath.SubstitutionSystems.SimplifiedHSS.SubstitutionSystems UniMath.SubstitutionSystems.Notation