Definition skewmonoidal_unitr_ax (V : skewmonoidal_data) {x y : V} (f : x --> y) : f · ρ' y = ρ' x · f #⊗ identity I := nat_trans_ax (skewmonoidal_unitr_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.