Lemma θ_nat_1_pointfree (X X' : [C, D']) (α : X --> X') (Z : Ptd) : compose (C := [C, D]) (# (functorial_composition _ _ _) ((nat_trans_id (pr1 (U Z)),,# H α): [C, C] ⊠ [C, D] ⟦(U Z,, H X), (U Z,, H X') ⟧)) (θ (X' ⊗ Z)) = θ (X ⊗ Z) · # H ( # (functorial_composition _ _ _) ((nat_trans_id (pr1 (U Z)),, α): [C, C] ⊠ [C, D'] ⟦(U Z,, X), (U Z,, X') ⟧) ). Proof. set (t := nat_trans_ax θ). set (t' := t (X ⊗ Z) (X' ⊗ Z)). set (t'' := t' (catbinprodmor α (identity _ ))). cbn in 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.