Definition lunitor_transf (a b : C) : bindelta_pair_functor (constant_functor (hom_precategory a b) (hom_precategory a a) (identity a)) (functor_identity (hom_precategory a b)) ∙ hcomp_functor ⟹ functor_identity (hom_precategory a b) := lunitor,, lunitor_natural a b.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.PrecategoryBinProduct.