Definition comp_cat_functor_empty_context_is_z_iso {C₁ C₂ : comp_cat} (F : comp_cat_functor C₁ C₂) : is_z_isomorphism (TerminalArrow [] (F [])). Proof. use make_is_z_isomorphism. - exact (comp_cat_functor_empty_context_arrow F []). - split. + use comp_cat_functor_empty_context_arrow_eq. + use TerminalArrowEq. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.Bicategories.ComprehensionCat.BicatOfCompCat.