Definition isTerminal_iso_comma (x : iso_comma F G) (H₁ : isTerminal C₁ (pr11 x)) (H₂ : isTerminal C₂ (pr21 x)) : isTerminal (iso_comma F G) x. Proof. intros w. use iscontraprop1. - abstract (use invproofirrelevance ; intros φ₁ φ₂ ; use eq_iso_comma_mor ; [ apply (@TerminalArrowEq _ (make_Terminal _ H₁)) | apply (@TerminalArrowEq _ (make_Terminal _ H₂)) ]). - refine ((TerminalArrow (_ ,, H₁) (pr11 w) ,, TerminalArrow (_ ,, H₂) (pr21 w)) ,, _). apply (@TerminalArrowEq _ (make_Terminal _ (HG _ 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.