Proposition cod_left_beck_chevalley_eq (φ : C/x) : cod_left_beck_chevalley_mor φ = dom_mor (left_beck_chevalley_nat_trans (is_right_adjoint_cod_fiber_functor HC f) (is_right_adjoint_cod_fiber_functor HC h) (comm_nat_z_iso HD f g h k p) φ). Proof. refine (!_). rewrite left_beck_chevalley_nat_trans_ob. rewrite !comp_in_cod_fib. etrans. { apply maponpaths. simpl. apply idpath. } etrans. { do 2 apply maponpaths_2. refine (dom_mor_comp_functor h _ @ _). rewrite (cod_fiber_functor_on_mor HC k). cbn. apply idpath. } etrans. { apply maponpaths_2. apply maponpaths. refine (dom_mor_comp_functor h _ @ _). etrans. { apply maponpaths. exact (comm_nat_z_iso_ob HD f g h k p _). } etrans. { apply (comp_in_cod_fib _ (fiber_functor_from_cleaving_comp_inv HD g h _)). } etrans. { apply maponpaths_2. apply comp_in_cod_fib. } etrans. { do 2 apply maponpaths. apply cod_fiber_functor_from_cleaving_comp_inv. } etrans. { apply maponpaths_2. etrans. { do 2 apply maponpaths. apply cod_fiber_functor_on_eq. } apply maponpaths_2. apply maponpaths. apply cod_fiber_functor_from_cleaving_comp. } cbn. apply idpath. } rewrite !assoc'. rewrite PullbackArrow_PullbackPr1. unfold cod_left_beck_chevalley_mor. use (MorphismsIntoPullbackEqual (isPullback_Pullback _)). - rewrite !assoc'. rewrite PullbackArrow_PullbackPr1. etrans. { do 3 apply maponpaths. apply PullbackArrow_PullbackPr1. } rewrite !PullbackArrow_PullbackPr1. rewrite !assoc. rewrite PullbackArrow_PullbackPr1. rewrite !assoc'. rewrite PullbackArrow_PullbackPr1. apply id_right. - rewrite !assoc'. rewrite PullbackArrow_PullbackPr2. etrans. { do 3 apply maponpaths. apply PullbackArrow_PullbackPr2. } rewrite !assoc. apply maponpaths_2. rewrite !assoc'. rewrite !PullbackArrow_PullbackPr2. 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.