Proposition comp_functor_counit_laws : is_nat_trans _ _ comp_functor_counit_data. Proof. intros g₁ g₂ h. use eq_mor_cod_fib. cbn -[fiber_category]. rewrite !comp_in_cod_fib. cbn. etrans. { apply (PullbackArrow_PullbackPr1 (HC y (pr1 g₂) x (pr2 g₂) f)). } rewrite transportf_cod_disp. cbn. 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.