proposition: 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: Proof. set (t := nat_trans_ax θ). set (t' := t (X ⊗ Z) (X' ⊗ Z)). set (t'' := t' (catbinprodmor α (identity _ ))). cbn 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