proposition: Lemma fbracket_natural (T : hss) {Z Z' : Ptd} (f : Z --> Z') (g : Z' --> ptd_from_alg T) : (` T ∘ # U f : EndC ⟦ `T • U Z , `T • U Z' ⟧) · ⦃ g ⦄ = ⦃ f · g ⦄.
proof: Proof. apply fbracket_unique_pointwise. - simpl. intro c. rewrite assoc. pose proof (nat_trans_ax (η T)) as H'. simpl in H'. rewrite <- H'; clear H'. rewrite <- assoc. apply maponpaths. pose proof (nat_trans_eq_weq (homset_property C) _ _ (fbracket_η T g)) as X. simpl in X. exact (X _ ). - intro c; simpl. assert (H':=nat_trans_ax (τ T)). simpl in H'. eapply pathscomp0. 2: apply assoc'. eapply pathscomp0. 2: { apply cancel_postcomposition. apply H'. } clear H'. set (H':=fbracket_τ T g). simpl in H'. assert (X:= nat_trans_eq_pointwise H' c). simpl in X. rewrite <- assoc. rewrite <- assoc. transitivity ( # (pr1 (H ((`T)))) (pr1 (pr1 f) c) · (pr1 (θ ((`T) ⊗ Z')) c)· pr1 (# H (fbracket T g)) c· pr1 (τ T) c). 2: { rewrite <- assoc. rewrite <- assoc. apply maponpaths. repeat rewrite assoc. apply X. } clear X. set (A:=θ_nat_2_pointwise). simpl in *. set (A':= A C C C H θ (`T) Z Z'). simpl in A'. set (A2:= A' f). clearbody A2; clear A'; clear A. rewrite A2; clear A2. repeat rewrite <- assoc. apply maponpaths. simpl. repeat rewrite assoc. apply cancel_postcomposition. rewrite (functor_comp H). apply cancel_postcomposition. clear H'. set (A:=horcomp_id_postwhisker C C C). rewrite A; try apply homset_property. apply idpath. Qed.
imports: UniMath.Foundations.PartD UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.PointedFunctors UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.HorizontalComposition UniMath.CategoryTheory.PointedFunctorsComposition UniMath.SubstitutionSystems.Signatures UniMath.SubstitutionSystems.Notation