Definition inv_square_profunctor : profunctor_square (functor_identity _) (functor_identity _) Q P. Proof. use make_profunctor_square. - exact (λ y x h, invmap (make_weq _ (Hτ y x)) h). - abstract (intros y₁ y₂ g x₁ x₂ f h ; cbn ; use (invmaponpathsweq (make_weq _ (Hτ _ _))) ; rewrite homotweqinvweq ; cbn ; rewrite (profunctor_square_lmap_rmap τ) ; cbn ; do 2 apply maponpaths ; refine (!_) ; apply (homotweqinvweq (make_weq _ (Hτ _ _)))). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Categories.CategoryOfSetCategories. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.Profunctors.Core. Require Import UniMath.CategoryTheory.Profunctors.Examples. Require Import UniMath.CategoryTheory.Profunctors.Transformation. Require Import UniMath.CategoryTheory.Profunctors.Squares. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Section FromProfunctorIso. End FromProfunctorIso.