Definition profunctor_square_laws {C₁ C₂ D₁ D₂ : category} {F : C₁ ⟶ C₂} {G : D₁ ⟶ D₂} {P : D₁ ↛ C₁} {Q : D₂ ↛ C₂} (τ : profunctor_square_data F G P Q) : UU := ∏ (y₁ y₂ : C₁) (x₁ x₂ : D₁) (g : y₂ --> y₁) (f : x₁ --> x₂) (h : P y₁ x₁), τ y₂ x₂ (lmap P g (rmap P f h)) = lmap Q (#F g) (rmap Q (#G f) (τ y₁ x₁ h)).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.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. Require Import UniMath.CategoryTheory.Profunctors.Examples. Require Import UniMath.CategoryTheory.Profunctors.Transformation.