Definition is_z_isomorphism_cod_left_beck_chevalley_mor (φ : C/x) : is_z_isomorphism (cod_left_beck_chevalley_mor φ). Proof. use make_is_z_isomorphism. - exact (cod_left_beck_chevalley_mor_inv φ). - split. + apply cod_left_beck_chevalley_mor_mor_inv. + apply cod_left_beck_chevalley_mor_inv_mor. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentSums.