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. 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.
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.