proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.DisplayedCats.Codomain UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod UniMath.CategoryTheory.DisplayedCats.DependentSums