Definition preserves_terminal_chosen_to_chosen {C₁ C₂ : category} (T₁ : Terminal C₁) (T₂ : Terminal C₂) (F : C₁ ⟶ C₂) (HF : is_z_isomorphism (TerminalArrow T₂ (F T₁))) : preserves_terminal F. Proof. use (preserves_terminal_if_preserves_chosen T₁). unfold preserves_chosen_terminal. use iso_to_Terminal. - exact T₂. - exact (z_iso_inv (_ ,, HF)). 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.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Pushouts. Require Import UniMath.CategoryTheory.Adjunctions.Core.