Proposition slice_parameterized_NNO_mor_Z : BinProductArrow _ _ (identity b) (TerminalArrow (codomain_fib_terminal x) b · slice_parameterized_NNO_Z) · slice_parameterized_NNO_mor = zy. Proof. unfold slice_parameterized_NNO_mor. use eq_mor_cod_fib. rewrite !comp_in_cod_fib. rewrite !assoc. refine (_ @ parameterized_NNO_mor_Z N _ _ (dom_mor zy) (dom_mor sy)). apply maponpaths_2. use BinProductArrowsEq. - rewrite BinProductPr1Commutes. rewrite !assoc'. etrans. { apply maponpaths. apply BinProductPr1Commutes. } etrans. { apply (PullbackArrow_PullbackPr1 (PC _ _ _ _ _)). } apply idpath. - rewrite BinProductPr2Commutes. rewrite !assoc'. etrans. { apply maponpaths. apply BinProductPr2Commutes. } etrans. { rewrite !assoc. apply maponpaths_2. apply (PullbackArrow_PullbackPr2 (PC _ _ _ _ _)). } rewrite comp_in_cod_fib. cbn. rewrite !id_right. rewrite !assoc'. rewrite BinProductPr2Commutes. rewrite !assoc. apply maponpaths_2. apply TerminalArrowEq. 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.