Definition enriched_profunctor_data_eq_weq_help {V : sym_mon_closed_cat} {C₁ C₂ : category} {E₁ : enrichment C₁ V} {E₂ : enrichment C₂ V} (P Q : E₁ ↛e E₂) : pr1 P ╝ pr1 Q ≃ ∑ (p : ∏ (y : C₂) (x : C₁), P y x = Q y x), (∏ (y₁ y₂ : C₂) (x : C₁), identity _ #⊗ idtoiso (p y₁ x) · lmap_e Q y₁ y₂ x = lmap_e P y₁ y₂ x · idtoiso (p y₂ x)) × (∏ (y : C₂) (x₁ x₂ : C₁), identity _ #⊗ idtoiso (p y x₁) · rmap_e Q y x₁ x₂ = rmap_e P y x₁ x₂ · idtoiso (p y x₂)). Proof. use weqbandf. - refine (_ ∘ weqtoforallpaths _ _ _)%weq. use weqonsecfibers ; intro y. apply weqtoforallpaths. - intro p ; cbn. induction P as [ P HP ]. induction P as [ Po Pm ]. induction Q as [ Q HQ ]. induction Q as [ Qo Qm ]. cbn in *. induction p ; cbn. refine (_ ∘ pathsdirprodweq)%weq. use weqdirprodf. + abstract (refine (_ ∘ weqtoforallpaths _ _ _)%weq ; use weqonsecfibers ; intro y₁ ; refine (_ ∘ weqtoforallpaths _ _ _)%weq ; use weqonsecfibers ; intro y₂ ; refine (_ ∘ weqtoforallpaths _ _ _)%weq ; use weqonsecfibers ; intro x ; cbn ; rewrite tensor_id_id ; rewrite id_left ; rewrite id_right ; cbn ; exact (weqpathsinv0 _ _)). + abstract (refine (_ ∘ weqtoforallpaths _ _ _)%weq ; use weqonsecfibers ; intro y₁ ; refine (_ ∘ weqtoforallpaths _ _ _)%weq ; use weqonsecfibers ; intro y₂ ; refine (_ ∘ weqtoforallpaths _ _ _)%weq ; use weqonsecfibers ; intro x ; cbn ; rewrite tensor_id_id ; rewrite id_left ; rewrite id_right ; cbn ; exact (weqpathsinv0 _ _)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.OppositeCategory.Core. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.Tensor. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.Profunctor. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.StandardProfunctors. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.ProfunctorTransformations. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.ProfunctorSquares. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed. Import MonoidalNotations.