Definition identitor_is_disp_univalent_2_0 (HD_2_1 : is_univalent_2_1 D) : disp_univalent_2_0 identitor_disp_cat. Proof. use disp_cell_unit_bicat_univalent_2_0. - apply map1cells_is_univalent_2_1. exact HD_2_1. - intros ; simpl. apply impred ; intro. apply D. - intro ; cbn. apply impred_isaset ; intro. apply D. - intros F Fid Fid' η ; cbn in *. apply funextsec ; intro X. induction η as [η₁ η₂]. specialize (η₁ X). specialize (η₂ X). rewrite !vassocr in η₁. rewrite vcomp_lunitor in η₁. rewrite !vassocl in η₁. rewrite rinvunitor_natural in η₁. rewrite <- rwhisker_hcomp in η₁. rewrite lunitor_runitor_identity, lunitor_V_id_is_left_unit_V_id in η₁. rewrite !vassocr in η₁. rewrite !runitor_rinvunitor, !id2_left in η₁. apply rwhisker_id_inj. 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.