Definition corestrict_full_image_local_equivalence : local_equivalence B₁_is_univalent_2_1 FI_is_univalent_2_1 corestrict_full_image. Proof. intros x y. use equiv_to_isadjequiv. simple refine ((_ ,, (_ ,, _)) ,, (_ ,, _)). - exact (corestrict_full_image_local_equivalence_right_adj x y). - use make_nat_trans. + exact (λ z, pr1 (left_adjoint_unit (F_local_equiv x y)) z). + abstract (intros a b g ; exact (pr2 (left_adjoint_unit (F_local_equiv x y)) _ _ g)). - use make_nat_trans. + exact (λ z, pr1 (left_adjoint_counit (F_local_equiv x y)) (pr1 z) ,, tt). + abstract (intros a b g ; use subtypePath ; [ intro ; apply isapropunit | ] ; exact (pr2 (left_adjoint_counit (F_local_equiv x y)) _ _ (pr1 g))). - apply is_nat_z_iso_to_is_invertible_2cell. intro z. exact (is_invertible_2cell_to_is_nat_z_iso _ (left_equivalence_unit_iso (F_local_equiv x y)) z). - apply is_nat_z_iso_to_is_invertible_2cell. intro z. apply is_inv2cell_to_is_z_iso. apply bicat_is_invertible_2cell_to_fullsub_is_invertible_2cell. apply (z_iso_to_inv2cell (_ ,, is_invertible_2cell_to_is_nat_z_iso _ (left_equivalence_counit_iso (F_local_equiv x y)) (pr1 z))). 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.