Definition cocartesian_initial_via_adj_to_cocartesian_initial_preserves {x y : B} (f : x --> y) : preserves_initial (pre_comp b f). Proof. use preserves_initial_if_preserves_chosen. - apply cocartesian_initial_via_adj_to_cocartesian_initial_obj. - use (iso_to_Initial (cocartesian_initial_via_adj_to_cocartesian_initial_obj x)). use inv2cell_to_z_iso. refine (comp_of_invertible_2cell (rwhisker_of_invertible_2cell _ _) (rassociator_invertible_2cell _ _ _)). apply (is_bifinal_invertible_2cell_property (pr2 T)). 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.