proposition: Lemma θ_nat_2_pointwise (X : [C, D']) (Z Z' : Ptd) (f : Z --> Z') (c : C) : # (pr1 (H X)) ((pr1 f) c) · pr1 (θ (X ⊗ Z')) c = pr1 (θ (X ⊗ Z)) c · pr1 (# H (identity X ⋆ pr1 f)) c .
proof: Proof. set (t := θ_nat_2 X _ _ f). set (t' := nat_trans_eq_weq (homset_property D) _ _ t c). clearbody t'; clear t. cbn in t'. unfold horcomp_data in t'. rewrite id_left in 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