Proposition slice_parameterized_NNO_eq : slice_parameterized_NNO_stable_mor = dom_mor (preserves_parameterized_NNO_mor (slice_parameterized_NNO N PC y) (slice_parameterized_NNO N PC x) (cod_pb PC f) (codomain_fib_preserves_terminal PC f)). Proof. unfold slice_parameterized_NNO_stable_mor. use (MorphismsIntoPullbackEqual (isPullback_Pullback (PC _ _ _ _ _))). - rewrite PullbackArrow_PullbackPr1. use BinProductArrowsEq. + etrans. { apply BinProductOfArrowsPr1. } refine (!_). rewrite !assoc'. etrans. { apply maponpaths. apply PullbackSqrCommutes. } rewrite !assoc. apply maponpaths_2. exact (mor_eq (preserves_parameterized_NNO_mor (slice_parameterized_NNO N PC y) (slice_parameterized_NNO N PC x) (cod_pb PC f) (codomain_fib_preserves_terminal PC f))). + etrans. { apply BinProductOfArrowsPr2. } rewrite id_right. refine (!_). rewrite !assoc'. use parameterized_NNO_mor_unique. * exact (TerminalArrow T x · parameterized_NNO_Z N). * exact (parameterized_NNO_S N). * pose (maponpaths dom_mor (preserves_parameterized_NNO_mor_Z (slice_parameterized_NNO N PC y) (slice_parameterized_NNO N PC x) (cod_pb PC f) (codomain_fib_preserves_terminal PC f))) as p. rewrite !comp_in_cod_fib in p. rewrite cod_fiber_functor_on_mor in p. etrans. { rewrite !assoc. do 2 apply maponpaths_2. exact p. } clear p. cbn. rewrite !assoc'. etrans. { apply maponpaths. rewrite !assoc. rewrite PullbackArrow_PullbackPr1. rewrite !assoc'. rewrite BinProductPr2Commutes. apply idpath. } rewrite !assoc. apply maponpaths_2. apply TerminalArrowEq. * pose (maponpaths dom_mor (preserves_parameterized_NNO_mor_S (slice_parameterized_NNO N PC y) (slice_parameterized_NNO N PC x) (cod_pb PC f) (codomain_fib_preserves_terminal PC f))) as p. rewrite !comp_in_cod_fib in p. rewrite cod_fiber_functor_on_mor in p. etrans. { rewrite !assoc. do 2 apply maponpaths_2. exact p. } clear p. rewrite !assoc'. apply maponpaths. cbn. rewrite !assoc. rewrite PullbackArrow_PullbackPr1. rewrite !assoc'. rewrite BinProductOfArrowsPr2. apply idpath. * rewrite BinProductPr2Commutes. apply idpath. * rewrite BinProductOfArrowsPr2. apply idpath. - rewrite PullbackArrow_PullbackPr2. refine (!_). exact (mor_eq (preserves_parameterized_NNO_mor (slice_parameterized_NNO N PC y) (slice_parameterized_NNO N PC x) (cod_pb PC f) (codomain_fib_preserves_terminal PC 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.