Corollary weak_equiv_preserves_chosen_terminal_eq {C D : category} (F : C ⟶ D) : is_weak_equiv F → is_univalent D → ∏ t1 t2, preserves_chosen_terminal_eq F t1 t2. Proof. intros Fw Duniv t1 t2. apply hinhpr. apply Duniv. set (Ft1_t := weak_equiv_preserves_terminal _ Fw _ (pr2 t1)). exact (z_iso_Terminals (_ ,, Ft1_t) t2). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.WeakEquivalences.Core. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Preservation.