Proposition form_adj_comp_cod_pb : form_adjunction comp_functor (cod_pb HC f) comp_functor_unit comp_functor_counit. Proof. split. - intro g. use eq_mor_cod_fib. rewrite comp_in_cod_fib. cbn. rewrite PullbackArrow_PullbackPr1. apply idpath. - intro g. use eq_mor_cod_fib. rewrite comp_in_cod_fib. use (MorphismsIntoPullbackEqual (isPullback_Pullback (HC y (pr1 g) x (pr2 g) f))). + rewrite !assoc'. etrans. { apply maponpaths. apply (PullbackArrow_PullbackPr1 (HC y (pr1 g) x (pr2 g) f)). } rewrite transportf_cod_disp. cbn. rewrite !assoc. rewrite PullbackArrow_PullbackPr1. apply idpath. + rewrite !assoc'. etrans. { apply maponpaths. apply (PullbackArrow_PullbackPr2 (HC y (pr1 g) x (pr2 g) f)). } cbn. rewrite !assoc. rewrite PullbackArrow_PullbackPr2. rewrite id_left, id_right. apply idpath. Qed.
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.Limits.Pullbacks. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. 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.DisplayedCats.Fiberwise.DependentSums.