Definition cod_fib_terminal_to_base_nat_trans {C₁ C₂ : category} (F : C₁ ⟶ C₂) (HF : preserves_terminal F) (T₁ : Terminal C₁) (T₂ := make_Terminal _ (HF _ (pr2 T₁))) : fiber_functor (disp_codomain_functor F) T₁ ∙ cod_fib_terminal_to_base T₂ ⟹ cod_fib_terminal_to_base T₁ ∙ F. Proof. use make_nat_trans. - exact (λ _, identity _). - abstract (intros x y f ; rewrite id_right, id_left ; cbn ; unfold dom_mor ; rewrite transportf_cod_disp ; apply idpath). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodLimits. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodColimits. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations.