Proposition codomain_functor_preserves_parameterized_NNO_eq : codomain_functor_preserves_parameterized_NNO_mor = dom_mor (preserves_parameterized_NNO_mor (slice_parameterized_NNO N₁ PC₁ x) (slice_parameterized_NNO N₂ PC₂ (F x)) (fiber_functor (disp_codomain_functor F) x) (preserves_terminal_fiber_disp_codomain_functor F x)). Proof. use (BinProductArrowsEq _ _ _ (preserves_binproduct_to_binproduct _ HF' (BC₁ x N₁))). - etrans. { unfold codomain_functor_preserves_parameterized_NNO_mor. rewrite !assoc'. apply maponpaths. apply BinProductPr1Commutes. } rewrite BinProductOfArrowsPr1. rewrite id_right. refine (!_). exact (mor_eq (preserves_parameterized_NNO_mor (slice_parameterized_NNO N₁ PC₁ x) (slice_parameterized_NNO N₂ PC₂ (F x)) (fiber_functor (disp_codomain_functor F) x) (preserves_terminal_fiber_disp_codomain_functor F x))). - etrans. { unfold codomain_functor_preserves_parameterized_NNO_mor. rewrite !assoc'. apply maponpaths. apply BinProductPr2Commutes. } rewrite BinProductOfArrowsPr2. refine (!_). use parameterized_NNO_mor_unique. + exact (#F (TerminalArrow _ x · parameterized_NNO_Z N₁)). + exact (#F (parameterized_NNO_S N₁)). + pose (maponpaths dom_mor (preserves_parameterized_NNO_mor_Z (slice_parameterized_NNO N₁ PC₁ x) (slice_parameterized_NNO N₂ PC₂ (F x)) (fiber_functor (disp_codomain_functor F) x) (preserves_terminal_fiber_disp_codomain_functor F x))) as p. rewrite !comp_in_cod_fib in p. etrans. { rewrite !assoc. apply maponpaths_2. exact p. } clear p. etrans. { apply maponpaths_2. apply maponpaths. apply disp_codomain_fiber_functor_mor. } cbn. rewrite !id_left. rewrite functor_id. rewrite id_left. rewrite <- functor_comp. apply maponpaths. apply BinProductPr2Commutes. + pose (maponpaths dom_mor (preserves_parameterized_NNO_mor_S (slice_parameterized_NNO N₁ PC₁ x) (slice_parameterized_NNO N₂ PC₂ (F x)) (fiber_functor (disp_codomain_functor F) x) (preserves_terminal_fiber_disp_codomain_functor F x))) as p. rewrite !comp_in_cod_fib in p. etrans. { rewrite !assoc. apply maponpaths_2. exact p. } clear p. rewrite !assoc'. apply maponpaths. etrans. { apply maponpaths_2. apply disp_codomain_fiber_functor_mor. } cbn. rewrite <- !functor_comp. apply maponpaths. apply BinProductOfArrowsPr2. + rewrite !assoc. rewrite BinProductPr2Commutes. rewrite !assoc'. rewrite preserves_parameterized_NNO_mor_Z. rewrite functor_comp. rewrite !assoc. apply maponpaths_2. apply TerminalArrowEq. + rewrite !assoc. rewrite BinProductOfArrowsPr2. rewrite !assoc'. rewrite preserves_parameterized_NNO_mor_S. 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.