Definition left_adjoint_equivalence_univ_cat_with_finlim {C₁ C₂ : univ_cat_with_finlim} (F : functor_finlim C₁ C₂) (HF : adj_equivalence_of_cats F) : left_adjoint_equivalence F. Proof. use equiv_to_adjequiv. simple refine ((_ ,, (_ ,, _)) ,, _ ,, _). - use make_functor_finlim. + exact (right_adjoint HF). + exact (right_adjoint_preserves_terminal _ HF). + exact (right_adjoint_preserves_pullback _ HF). - use make_nat_trans_finlim. exact (unit_nat_z_iso_from_adj_equivalence_of_cats HF). - use make_nat_trans_finlim. exact (counit_nat_z_iso_from_adj_equivalence_of_cats HF). - use is_invertible_2cell_cat_with_finlim. apply (unit_nat_z_iso_from_adj_equivalence_of_cats HF). - use is_invertible_2cell_cat_with_finlim. apply (counit_nat_z_iso_from_adj_equivalence_of_cats HF). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.PullbackConstructions. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.Limits.PreservationProperties. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod. Require Import UniMath.CategoryTheory.LocallyCartesianClosed.LocallyCartesianClosed. Require Import UniMath.CategoryTheory.LocallyCartesianClosed.Preservation. Require Import UniMath.CategoryTheory.SubobjectClassifier.SubobjectClassifier. Require Import UniMath.CategoryTheory.SubobjectClassifier.SubobjectClassifierIso. Require Import UniMath.CategoryTheory.SubobjectClassifier.PreservesSubobjectClassifier. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sub1Cell. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Prod. := BinProductsFromPullbacks