Proposition comp_functor_unit_laws : is_nat_trans _ _ comp_functor_unit_data. Proof. intros g₁ g₂ h. use eq_mor_cod_fib. cbn -[fiber_category]. rewrite !comp_in_cod_fib. cbn. use (MorphismsIntoPullbackEqual (isPullback_Pullback _)). - rewrite !assoc'. rewrite PullbackArrow_PullbackPr1. refine (!_). etrans. { apply maponpaths. apply (PullbackArrow_PullbackPr1 (HC y (cod_dom g₂) x (cod_mor g₂ · f) f)). } rewrite transportf_cod_disp. cbn. rewrite !assoc. rewrite PullbackArrow_PullbackPr1. rewrite id_left, id_right. apply idpath. - rewrite !assoc'. rewrite PullbackArrow_PullbackPr2. refine (!_). etrans. { apply maponpaths. apply (PullbackArrow_PullbackPr2 (HC y (cod_dom g₂) x (cod_mor g₂ · f) f)). } cbn. rewrite !assoc. rewrite PullbackArrow_PullbackPr2. refine (_ @ !(mor_eq h)). apply id_right. 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.