Definition adj_equiv_preserves_bincoproducts_f (P : BinCoproducts C₁) : BinCoproducts C₂. Proof. intros x y. pose (H := pr2 (P (R x) (R y))). pose (prod := make_BinCoproduct _ _ _ _ _ _ (left_adjoint_preserves_bincoproduct _ HL _ _ _ _ _ H)). use (BinCoproduct_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.