Definition fiber_is_left_adj {D D' : disp_cat C} {FF : disp_functor (functor_identity _) D D'} (EFF : right_adjoint_over_id FF) (c : C) : is_left_adjoint (fiber_functor FF c). Proof. destruct EFF as [[GG [η ε]] axs]; simpl in axs. exists (fiber_functor GG _). exists (fiber_nat_trans η _,, fiber_nat_trans ε _). use tpair; cbn. + unfold triangle_1_statement. intros d; cbn. set (thisax := pr1 axs c d); clearbody thisax; clear axs. etrans. apply maponpaths, thisax. etrans. apply transport_f_b. use (@maponpaths_2 _ _ _ _ _ (paths_refl _)). apply homset_property. + unfold triangle_2_statement. intros d; cbn. set (thisax := pr2 axs c d); clearbody thisax; clear axs. etrans. apply maponpaths, thisax. etrans. apply transport_f_b. use (@maponpaths_2 _ _ _ _ _ (paths_refl _)). apply homset_property. Defined.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. 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.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber.