Proposition isaprop_is_disp_nat_z_iso {C₁ C₂ : category} {F G : C₁ ⟶ C₂} {τ : nat_z_iso F G} {D₁ : disp_cat C₁} {D₂ : disp_cat C₂} {FF : disp_functor F D₁ D₂} {GG : disp_functor G D₁ D₂} (ττ : disp_nat_trans τ FF GG) : isaprop (is_disp_nat_z_iso τ ττ). Proof. repeat (use impred ; intro). apply isaprop_is_z_iso_disp. Qed.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Isos.