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. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.BicatOfCatsElementary. Require Import UniMath.SubstitutionSystems.Notation.