Library UniMath.Bicategories.Grothendieck.FiberwiseEquiv

Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Adjunctions.Core.
Require Import UniMath.CategoryTheory.Equivalences.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.
Require Import UniMath.CategoryTheory.DisplayedCats.Functors.
Require Import UniMath.CategoryTheory.DisplayedCats.Fiber.
Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
Require Import UniMath.Bicategories.Core.Bicat.
Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.EquivToAdjequiv.
Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats.
Require Import UniMath.Bicategories.Core.Examples.FibSlice.
Require Import UniMath.Bicategories.Morphisms.Adjunctions.
Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor.
Import PseudoFunctor.Notations.
Require Import UniMath.Bicategories.PseudoFunctors.Examples.Identity.
Require Import UniMath.Bicategories.PseudoFunctors.Examples.Composition.
Require Import UniMath.Bicategories.Transformations.PseudoTransformation.
Require Import UniMath.Bicategories.PseudoFunctors.Biequivalence.
Require Import UniMath.Bicategories.Grothendieck.Biequivalence.

Local Open Scope cat.

Definition fiberwise_equiv_to_adjequiv
           {C : univalent_category}
           {P₁ P₂ : fib_slice_bicat C}
           (F : P₁ --> P₂)
           (HF : ∏ (x : C ), adj_equivalence_of_cats (fiber_functor (pr1 F) x))
  : left_adjoint_equivalence F.
Show proof.

  use (biequiv_reflect_adjequiv (grothendieck_construction C)).
  use pointwise_adjequiv_to_adjequiv.
  - exact univalent_cat_is_univalent_2.
  - intros x ; cbn.
    use equiv_cat_to_adj_equiv.
    exact (HF x).

Definition ff_and_eso_to_adjequiv
           {C : univalent_category}
           {P₁ P₂ : fib_slice_bicat C}
           (F : P₁ --> P₂)
           (F_full : ∏ (x : C ), full (fiber_functor (pr1 F) x))
           (F_faithful : ∏ (x : C ), faithful (fiber_functor (pr1 F) x))
           (F_eso : ∏ (x : C ), Functors.essentially_surjective (fiber_functor (pr1 F) x))
  : left_adjoint_equivalence F.
Show proof.

  use fiberwise_equiv_to_adjequiv.
  intro x.
  use rad_equivalence_of_cats.
  - use is_univalent_fiber.
    apply (pr1 P₁).
  - use full_and_faithful_implies_fully_faithful.
    split.
    + exact (F_full x).
    + exact (F_faithful x).
  - exact (F_eso x).