Definition preserves_parameterized_NNO_prod_independent {C₁ C₂ : univalent_category} {T₁ : Terminal C₁} {BC₁ BC₁' : BinProducts C₁} {T₂ : Terminal C₂} {BC₂ BC₂' : BinProducts C₂} {N₁ : parameterized_NNO T₁ BC₁} {N₂ : parameterized_NNO T₂ BC₂} {F : C₁ ⟶ C₂} {HF : preserves_terminal F} (HFN : preserves_parameterized_NNO N₁ N₂ F HF) : preserves_parameterized_NNO (parameterized_NNO_prod_independent BC₁' N₁) (parameterized_NNO_prod_independent BC₂' N₂) F HF.
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.