Definition disp_left_equivalence_to_total {B : bicat} {D : disp_bicat B} {x y : B} {f : x --> y} {Hf : left_equivalence f} {xx : D x} {yy : D y} {ff : xx -->[ f ] yy} (Hff : disp_left_equivalence Hf ff) : @left_equivalence (total_bicat D) (x ,, xx) (y ,, yy) (f ,, ff). Proof. simple refine (_ ,, _). - exact (left_adjoint_data_disp_to_total ff (pr1 Hf ,, pr1 Hff)). - use (left_equivalence_axioms_disp_to_total _ (_ ,, _)). + exact (pr2 Hf). + exact (pr2 Hff). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.Core.Univalence.