Definition map2cells_is_disp_univalent_2_0 (HD_2_1 : is_univalent_2_1 D) : disp_univalent_2_0 map2cells_disp_cat. Proof. use disp_cell_unit_bicat_univalent_2_0. - apply map1cells_is_univalent_2_1. exact HD_2_1. - intros ; simpl. repeat (apply impred ; intro). apply D. - intro ; cbn. repeat (apply impred_isaset ; intro). apply D. - intros F F₂ F₂' η ; cbn in *. induction η as [η₁ η₂]. apply funextsec ; intro X. apply funextsec ; intro Y. apply funextsec ; intro f. apply funextsec ; intro g. apply funextsec ; intro α. specialize (η₁ X Y f g α). specialize (η₂ X Y f g α). rewrite !vassocr in η₁. rewrite vcomp_lunitor in η₁. rewrite !vassocl in η₁. rewrite rinvunitor_natural in η₁. rewrite <- rwhisker_hcomp in η₁. rewrite !vassocr in η₁. apply rwhisker_id_inj. use (vcomp_lcancel (lunitor _ • rinvunitor _)). { is_iso. } exact (!η₁). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.PseudoFunctors.Display.Base. Require Import UniMath.Bicategories.PseudoFunctors.Display.Map1Cells. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.DisplayedBicats.Examples.DisplayedCatToBicat. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence.