Definition codomain_functor_preserves_parameterized_NNO_mor : BC₂ (F x) N₂ --> F (BC₁ x N₁) := BinProductOfArrows _ _ _ (identity _) (preserves_parameterized_NNO_mor N₁ N₂ _ HF) · inv_from_z_iso (preserves_binproduct_to_z_iso F HF' (BC₁ x N₁) (BC₂ (F x) (F N₁))).
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.