Definition comp_profunctor_ob_in {z : C₃} (y : C₂) {x : C₁} (h₁ : P y x) (h₂ : Q z y) : comp_profunctor_ob z x := HSET_coend_in (comp_profunctor_colim_profunctor x z) y (h₁ ,, h₂).
Require Import UniMath.Foundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.Categories.HSET.SetCoends. Require Import UniMath.CategoryTheory.Profunctors.Core.