Proposition comp_preserves_parameterized_NNO_eq : preserves_parameterized_NNO_mor N₂ N₃ G HG · # G (preserves_parameterized_NNO_mor N₁ N₂ F HF) = preserves_parameterized_NNO_mor N₁ N₃ (F ∙ G) (composition_preserves_terminal HF HG). Proof. use is_NNO_parameterized_NNO_unique. - exact (TerminalArrow (preserves_terminal_to_terminal _ (composition_preserves_terminal HF HG) T₁) _ · #G(#F(parameterized_NNO_Z N₁))). - exact (#G(#F(parameterized_NNO_S N₁))). - rewrite !assoc. rewrite preserves_parameterized_NNO_mor_Z. rewrite !assoc'. etrans. { apply maponpaths. exact (!(functor_comp G _ _)). } etrans. { do 2 apply maponpaths. apply preserves_parameterized_NNO_mor_Z. } rewrite functor_comp. rewrite !assoc. apply maponpaths_2. apply (TerminalArrowEq (T := preserves_terminal_to_terminal _ _ _)). - rewrite !assoc. rewrite preserves_parameterized_NNO_mor_S. rewrite !assoc'. etrans. { apply maponpaths. exact (!(functor_comp G _ _)). } etrans. { do 2 apply maponpaths. apply preserves_parameterized_NNO_mor_S. } rewrite functor_comp. apply idpath. - exact (preserves_parameterized_NNO_mor_Z N₁ N₃ _ (composition_preserves_terminal HF HG)). - exact (preserves_parameterized_NNO_mor_S N₁ N₃ _ (composition_preserves_terminal HF HG)). Qed.
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.Preservation. Require Import UniMath.CategoryTheory.Arithmetic.NNO.