Definition comp_functor_unit_data : nat_trans_data (functor_identity (C / x)) (comp_functor ∙ cod_pb HC f). Proof. simple refine (λ g, make_cod_fib_mor _ _). - use PullbackArrow. + exact (identity (cod_dom g)). + exact (cod_mor g). + abstract (cbn ; apply id_left). - abstract (cbn ; rewrite PullbackArrow_PullbackPr2 ; apply idpath). Defined.
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.