Definition isInitial_iso_comma (x : iso_comma F G) (H₁ : isInitial C₁ (pr11 x)) (H₂ : isInitial C₂ (pr21 x)) : isInitial (iso_comma F G) x. Proof. intros w. use iscontraprop1. - abstract (use invproofirrelevance ; intros φ₁ φ₂ ; use eq_iso_comma_mor ; [ apply (@InitialArrowEq _ (make_Initial _ H₁)) | apply (@InitialArrowEq _ (make_Initial _ H₂)) ]). - refine ((InitialArrow (_ ,, H₁) (pr11 w) ,, InitialArrow (_ ,, H₂) (pr21 w)) ,, _). apply (@InitialArrowEq _ (make_Initial _ (HF _ H₁))). 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.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.IsoCommaCategory. 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.