Definition idtoiso_2_0_is_idtoiso_id_2_0_alt (x y : E) : @idtoiso_2_0 E x y ~ idtoiso_2_0_alt (pr2 x) (pr2 y). Proof. intros p. induction p. use total2_paths_b. - reflexivity. - use subtypePath. + intro. apply isapropdirprod. * apply isapropdirprod ; apply E. * apply isapropdirprod ; apply isaprop_is_invertible_2cell. + reflexivity. 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.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations.