Definition cocartesian_coprod_weq_cocartesian_coprod_via_adj (HB : is_univalent_2_1 B) : cocartesian_coprod b ≃ cocartesian_coprod_via_adj b prod. Proof. use weqimplimpl. - exact cocartesian_coprod_to_cocartesian_coprod_via_adj. - exact cocartesian_coprod_via_adj_to_cocartesian_coprod. - apply isaprop_cocartesian_coprod. exact HB. - apply isaprop_cocartesian_coprod_via_adj. exact HB. 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.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.UnivalenceOp. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Limits.Final. Require Import UniMath.Bicategories.Limits.Products. Section FromAdj. End FromAdj. Section FromAdj. End FromAdj.