Definition adj_equiv_preserves_binproducts_b (P : BinProducts C₂) : BinProducts C₁. Proof. intros x y. pose (H := pr2 (P (L x) (L y))). pose (prod := make_BinProduct _ _ _ _ _ _ (right_adjoint_preserves_binproduct _ HL _ _ _ _ _ H)). use (BinProduct_z_iso_lr prod). - apply (nat_z_iso_pointwise_z_iso η). - apply (nat_z_iso_pointwise_z_iso η). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.Limits.LimitIso. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.CompositesAndInverses.