Definition profunctor_to_discrete_twosided_fibration : discrete_twosided_fibration C₂ C₁. Proof. simple refine (_ ,, _ ,, _ ,, _). - exact profunctor_to_twosided_disp_cat. - exact discrete_profunctor_to_twosided_disp_cat. - intros x₁ x₂ y xy₂ f. simple refine (_ ,, _ ,, _). + exact (lmap P f xy₂). + abstract (cbn -[lmap rmap] ; rewrite rmap_id ; apply idpath). + abstract (cbn ; intro ; intros ; cbn -[lmap rmap] in * ; rewrite id_right in fg' ; rewrite fg' ; rewrite lmap_comp ; apply idpath). - intros y x₁ x₂ xy₂ f. simple refine (_ ,, _ ,, _). + exact (rmap P f xy₂). + abstract (cbn -[lmap rmap] ; rewrite lmap_id ; apply idpath). + abstract (cbn ; intro ; intros ; cbn -[lmap rmap] in * ; rewrite id_left in fg' ; rewrite <- fg' ; rewrite rmap_comp ; apply idpath). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.Profunctors.Core. 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. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedFibration.