Proposition slice_parameterized_NNO_stable_is_z_iso_inverses : is_inverse_in_precat slice_parameterized_NNO_stable_mor slice_parameterized_NNO_stable_inv. Proof. unfold slice_parameterized_NNO_stable_mor, slice_parameterized_NNO_stable_inv. split. - use BinProductArrowsEq. + rewrite id_left. rewrite !assoc'. rewrite BinProductPr1Commutes. apply PullbackArrow_PullbackPr2. + rewrite id_left. rewrite !assoc'. rewrite BinProductPr2Commutes. rewrite !assoc. rewrite PullbackArrow_PullbackPr1. rewrite BinProductOfArrowsPr2. apply id_right. - use (MorphismsIntoPullbackEqual (isPullback_Pullback (PC _ _ _ _ _))). + rewrite id_left. rewrite !assoc'. rewrite PullbackArrow_PullbackPr1. use BinProductArrowsEq. * rewrite !assoc'. rewrite BinProductOfArrowsPr1. rewrite !assoc. rewrite BinProductPr1Commutes. refine (!_). apply PullbackSqrCommutes. * rewrite !assoc'. rewrite BinProductOfArrowsPr2. rewrite id_right. rewrite BinProductPr2Commutes. apply idpath. + rewrite id_left. rewrite !assoc'. rewrite PullbackArrow_PullbackPr2. rewrite BinProductPr1Commutes. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.Arithmetic.ParameterizedNNO. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodLimits. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodFunctor.