fact: Definition lmap_comp {C₁ C₂ : category} (P : profunctor C₁ C₂) {x : C₁} {y₁ y₂ y₃ : C₂} (g₁ : y₁ --> y₂) (g₂ : y₂ --> y₃) (z : P y₃ x) : lmap P (g₁ · g₂) z = lmap P g₁ (lmap P g₂ z).
imports: UniMath.Foundations.Preamble UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Categories.HSET.All