Proposition slice_parameterized_NNO_mor_S : BinProductOfArrows _ _ _ (identity b) slice_parameterized_NNO_S · slice_parameterized_NNO_mor = slice_parameterized_NNO_mor · sy. Proof. unfold slice_parameterized_NNO_mor. use eq_mor_cod_fib. rewrite !comp_in_cod_fib. refine (!_). etrans. { cbn. rewrite !assoc'. apply maponpaths. exact (!(parameterized_NNO_mor_S N _ _ (dom_mor zy) (dom_mor sy))). } rewrite !assoc. apply maponpaths_2. use BinProductArrowsEq. - rewrite !assoc'. rewrite BinProductOfArrowsPr1. rewrite id_right. rewrite BinProductPr1Commutes. refine (!_). etrans. { apply maponpaths. apply BinProductPr1Commutes. } etrans. { apply (PullbackArrow_PullbackPr1 (PC _ _ _ _ _)). } rewrite id_right. apply idpath. - rewrite !assoc'. rewrite BinProductOfArrowsPr2. rewrite !assoc. rewrite BinProductPr2Commutes. refine (!_). rewrite !assoc'. etrans. { apply maponpaths. apply BinProductPr2Commutes. } rewrite !assoc. etrans. { apply maponpaths_2. apply (PullbackArrow_PullbackPr2 (PC _ _ _ _ _)). } rewrite !comp_in_cod_fib ; cbn. rewrite !assoc'. rewrite BinProductOfArrowsPr2. 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.