Definition cod_fib_terminal_to_base_nat_z_iso {C₁ C₂ : category} (F : C₁ ⟶ C₂) (HF : preserves_terminal F) (T₁ : Terminal C₁) (T₂ := make_Terminal _ (HF _ (pr2 T₁))) : nat_z_iso (fiber_functor (disp_codomain_functor F) T₁ ∙ cod_fib_terminal_to_base T₂) (cod_fib_terminal_to_base T₁ ∙ F). Proof. use make_nat_z_iso. - exact (cod_fib_terminal_to_base_nat_trans F HF T₁). - intro. 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.