proposition: Lemma θ_nat_1_pointwise (X X' : [C, D']) (α : X --> X') (Z : Ptd) (c : C) : pr1 (# H α) ((pr1 Z) c) · pr1 (θ (X' ⊗ Z)) c = pr1 (θ (X ⊗ Z)) c · pr1 (# H (α ⋆ nat_trans_id (pr1 Z))) c.
proof: Proof. assert (t := θ_nat_1 _ _ α Z). assert (t' := nat_trans_eq_weq (homset_property D) _ _ t c). clear t. cbn in t'. unfold horcomp_data in t'. etrans; [| exact t' ]. clear t'. apply pathsinv0. etrans. { apply cancel_postcomposition. apply maponpaths. apply functor_id. } rewrite <- assoc. rewrite id_left. apply idpath. 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