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).
Require Import UniMath.Foundations.Preamble. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Categories.HSET.All.