Lemma weak_equiv_lifts_preserves_terminal {C1 C2 C3 : category} (F : C1 ⟶ C3) (G : C1 ⟶ C2) (H : C2 ⟶ C3) (α : nat_z_iso (G ∙ H) F) (Gw : is_weak_equiv G) (Fpterm : preserves_terminal F) : preserves_terminal H. Proof. intros x2 x2_is_term. use (factor_through_squash _ _ (eso_from_weak_equiv _ Gw x2)). { apply isaprop_isTerminal. } intros [x1 i] y3. use (iscontrweqb' (Y := (C3⟦y3, H(G x1)⟧))). + use (iscontrweqb' (Y := (C3⟦y3, F x1⟧))). * use (Fpterm _ _). use (weak_equiv_reflects_terminal _ Gw). exact (iso_to_Terminal (_,, x2_is_term) _ (z_iso_inv i)). * apply z_iso_comp_left_weq. exact (_ ,, pr2 α x1). + apply z_iso_comp_left_weq. apply functor_on_z_iso. exact (z_iso_inv i). 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. Require Import UniMath.CategoryTheory.WeakEquivalences.Terminal. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Core.Examples.BicatOfCats. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.Bicategories.PseudoFunctors.UniversalArrow. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.PseudoFunctors.Examples.BicatOfCatToUnivCat. Require Import UniMath.Bicategories.DisplayedBicats.Examples.DispBicatOnCatToUniv. Require Import UniMath.Bicategories.DisplayedBicats.Examples.CategoriesWithStructure. Require Import UniMath.Bicategories.DisplayedBicats.DisplayedUniversalArrow. Require Import UniMath.Bicategories.DisplayedBicats.DisplayedUniversalArrowOnCat.