Definition pr2_preserves_initial (C₁ C₂ : category) : preserves_initial (pr2_functor C₁ C₂). Proof. intros x Hx w. use iscontraprop1. - abstract (use invproofirrelevance ; intros φ₁ φ₂ ; refine (maponpaths dirprod_pr2 (InitialArrowUnique (x ,, Hx) (pr1 x ,, w) (identity _ ,, φ₁)) @ !_) ; exact (maponpaths dirprod_pr2 (InitialArrowUnique (x ,, Hx) (pr1 x ,, w) (identity _ ,, φ₂)))). - exact (pr2 (InitialArrow (_ ,, Hx) (pr1 x ,, w))). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Preservation.