proposition: 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: Proof. repeat (use impred ; intro). apply isaprop_is_z_iso_disp. Qed.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Isos