Proposition preserves_initial_fiber_disp_codomain_functor {C₁ C₂ : category} (I : Initial C₁) (F : C₁ ⟶ C₂) (HF : preserves_initial F) (x : C₁) : preserves_initial (fiber_functor (disp_codomain_functor F) x). Proof. use preserves_initial_if_preserves_chosen. - exact (initial_cod_fib x I). - use (iso_to_Initial (initial_cod_fib _ (make_Initial _ (HF _ (pr2 I))))). use z_iso_fiber_from_z_iso_disp. use make_z_iso_disp. + use make_cod_fib_mor. * apply identity. * abstract (use InitialArrowEq). + use is_z_iso_disp_codomain. apply is_z_isomorphism_identity. 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.