Definition comp_cat_extend_over_iso {C : comp_cat} {Γ₁ Γ₂ : C} (A : ty Γ₁) (s : Γ₂ --> Γ₁) (Hs : is_z_isomorphism s) : z_iso (Γ₂ & (A [[ s ]])) (Γ₁ & A) := from_z_iso_disp_codomain (disp_functor_on_z_iso_disp (comp_cat_comprehension C) (comp_cat_iso_subst A (s ,, Hs))).
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.