Definition codomain_functor_preserves_parameterized_NNO_iso : is_z_isomorphism (BinProductOfArrows _ (BC₂ (F x) (F N₁)) (BC₂ (F x) N₂) (identity (F x)) (preserves_parameterized_NNO_mor N₁ N₂ F HF)). Proof. use make_is_z_isomorphism. - exact (BinProductOfArrows _ _ _ (identity _) (is_z_isomorphism_mor HFN)). - abstract (split ; rewrite BinProductOfArrows_comp ; rewrite id_left ; refine (_ @ BinProductOfArrows_id _ _ _ _) ; apply maponpaths ; apply HFN). Defined.
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.