Proposition slice_parameterized_NNO_unique : isaprop (∑ (f : codomain_fib_binproducts PC x b slice_parameterized_NNO_ob --> y), (BinProductArrow _ _ (identity b) (TerminalArrow (codomain_fib_terminal x) b · slice_parameterized_NNO_Z) · f = zy) × (BinProductOfArrows _ _ _ (identity b) slice_parameterized_NNO_S · f = f · sy)). Proof. use invproofirrelevance. intros f₁ f₂. use subtypePath. { intro. use isapropdirprod ; apply homset_property. } use (cancel_precomposition_z_iso slice_parameterized_NNO_mor_dom_iso). use eq_mor_cod_fib. rewrite !comp_in_cod_fib. use parameterized_NNO_mor_unique. - exact (dom_mor zy). - exact (dom_mor sy). - apply slice_parameterized_NNO_unique_Z. exact (pr12 f₁). - apply slice_parameterized_NNO_unique_S. exact (pr22 f₁). - apply slice_parameterized_NNO_unique_Z. exact (pr12 f₂). - apply slice_parameterized_NNO_unique_S. exact (pr22 f₂). 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.