proposition: Lemma θ_nat_2 (X : [C, D']) (Z Z' : Ptd) (f : Z --> Z') : compose (C := [C, D]) (identity (H X) ⋆ pr1 f) (θ (X ⊗ Z')) = θ (X ⊗ Z) · # H (identity X ⋆ pr1 f).
proof: Proof. set (t := nat_trans_ax θ). set (t' := t (X ⊗ Z) (X ⊗ Z') (catbinprodmor (identity _ ) f)). rewrite (@horcomp_post_pre _ _ D). rewrite (@horcomp_post_pre _ _ D'). cbn in t'. unfold catbinprodmor in t'. cbn in t'. set (T := functor_id H X). cbn in *. rewrite T in t'. clear T. exact t'. Qed.
imports: UniMath.Foundations.PartD UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.PointedFunctors UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.HorizontalComposition UniMath.CategoryTheory.BicatOfCatsElementary UniMath.SubstitutionSystems.Notation