Definition skewmonoidal_unitl_ax (V : skewmonoidal_data) {x y : V} (f : x --> y) : (identity I) #⊗ f · λ' y = λ' x · f := nat_trans_ax (skewmonoidal_unitl_nt V) _ _ f.
Require Import UniMath.Foundations.PartD. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.ProductCategory. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.whiskering.