Definition pr1_preserves_terminal (C₁ C₂ : category) : preserves_terminal (pr1_functor C₁ C₂). Proof. intros x Hx w. use iscontraprop1. - abstract (use invproofirrelevance ; intros φ₁ φ₂ ; refine (maponpaths pr1 (TerminalArrowUnique (x ,, Hx) (w ,, pr2 x) (φ₁ ,, identity _)) @ !_) ; exact (maponpaths pr1 (TerminalArrowUnique (x ,, Hx) (w ,, pr2 x) (φ₂ ,, identity _)))). - exact (pr1 (TerminalArrow (_ ,, Hx) (w ,, pr2 x))). 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.