Definition corestrict_full_image_local_equivalence_right_adj (x y : B₁) : bicat_of_univ_cats ⟦ univ_hom FI_is_univalent_2_1 (corestrict_full_image x) (corestrict_full_image y), univ_hom B₁_is_univalent_2_1 x y ⟧. Proof. pose (G := F_local_equiv x y). use make_functor. - use make_functor_data. + exact (λ z, pr1 (left_adjoint_right_adjoint G) (pr1 z)). + exact (λ _ _ f, # (pr1 (left_adjoint_right_adjoint G)) (pr1 f)). - split. + abstract (intro a ; exact (functor_id (left_adjoint_right_adjoint G) (pr1 a))). + abstract (intros ? ? ? f g ; exact (functor_comp (left_adjoint_right_adjoint G) (pr1 f) (pr1 g))). 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.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Examples.Image. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.DisplayedBicats.Examples.FullSub. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.PseudoFunctors.Properties.