Proposition weak_equiv_preserves_chosen_terminal {C D : category} (F : C ⟶ D) : is_weak_equiv F → ∏ t : Terminal C, preserves_chosen_terminal t F. Proof. intros Fw [x x_is_t] y'. use (factor_through_squash (isapropiscontr _) _ (eso_from_weak_equiv _ Fw y')). intros [y yi]. apply (iscontrweqb' (x_is_t y)). refine (invweq (_ ,, ff_from_weak_equiv _ Fw y x) ∘ _)%weq. apply z_iso_comp_right_weq. exact yi. 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.