proposition: Lemma weak_equiv_lifts_preserves_chosen_binproducts_eq {C1 : category} (C2 C3 : univalent_category) {F : C1 ⟶ C3} {G : C1 ⟶ C2} {H : C2 ⟶ C3} (α : nat_z_iso (G ∙ H) F) (C1_prod : BinProducts C1) (C2_prod : BinProducts (pr1 C2)) (C3_prod : BinProducts (pr1 C3)) (Gw : is_weak_equiv G) : preserves_chosen_binproducts_eq F C1_prod C3_prod → preserves_chosen_binproducts_eq H C2_prod C3_prod.
proof: Proof. intros Fprod y1 y2. use (factor_through_squash _ _ (eso_from_weak_equiv _ Gw y1)). { apply isapropishinh. } intros [x1 i1]. use (factor_through_squash _ _ (eso_from_weak_equiv _ Gw y2)). { apply isapropishinh. } intros [x2 i2]. unfold preserves_chosen_binproducts_eq in Fprod. use (factor_through_squash _ _ (Fprod x1 x2)). { apply isapropishinh. } intro p. pose (ϕ₁ := nat_z_iso_pointwise_z_iso α x1). pose (ϕ₂ := nat_z_iso_pointwise_z_iso α x2). pose (ϕ₃ := nat_z_iso_pointwise_z_iso α (C1_prod x1 x2)). pose (ψ₁ := isotoid _ (pr2 C3) ϕ₁). pose (ψ₂ := isotoid _ (pr2 C3) ϕ₂). pose (ψ₃ := isotoid _ (pr2 C3) ϕ₃). pose (j1 := isotoid _ (pr2 C2) i1). pose (j2 := isotoid _ (pr2 C2) i2). set (Gprod := weak_equiv_preserves_binproducts_eq Gw (pr2 C2) C1_prod C2_prod). use (factor_through_squash _ _ (Gprod x1 x2)). { apply isapropishinh. } intro Gx1x2. clear Gprod. apply hinhpr. rewrite <- j1, <- j2. etrans. { apply maponpaths. exact (! Gx1x2). } refine (ψ₃ @ _). refine (p @ _). refine (maponpaths (fun z => BinProductObject _ (C3_prod z _)) _ @ _). { exact (! ψ₁). } refine (maponpaths (fun z => BinProductObject _ (C3_prod _ z)) _). exact (! ψ₂). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Equivalences.CompositesAndInverses UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Equivalences.FullyFaithful UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Adjunctions UniMath.CategoryTheory.DisplayedCats.Equivalences UniMath.CategoryTheory.DisplayedCats.TotalAdjunction UniMath.CategoryTheory.WeakEquivalences UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Preservation UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.Examples.BicatOfUnivCats UniMath.Bicategories.Core.Examples.BicatOfCats UniMath.Bicategories.Core.Univalence UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.DisplayedBicats.DispPseudofunctor UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat UniMath.Bicategories.PseudoFunctors.PseudoFunctor UniMath.Bicategories.Transformations.PseudoTransformation UniMath.Bicategories.PseudoFunctors.Biadjunction UniMath.Bicategories.Modifications.Modification UniMath.Bicategories.PseudoFunctors.UniversalArrow UniMath.Bicategories.DisplayedBicats.DispBiadjunction UniMath.Bicategories.DisplayedBicats.DispInvertibles UniMath.Bicategories.PseudoFunctors.Examples.BicatOfCatToUnivCat UniMath.Bicategories.DisplayedBicats.Examples.DispBicatOnCatToUniv UniMath.Bicategories.DisplayedBicats.Examples.CategoriesWithStructure UniMath.Bicategories.DisplayedBicats.DisplayedUniversalArrow UniMath.Bicategories.DisplayedBicats.DisplayedUniversalArrowOnCat