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. 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.
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.BinProducts. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.WeakEquivalences.Reflection.BinProducts. Require Import UniMath.CategoryTheory.WeakEquivalences.Preservation.Binproducts.