Definition from_biinitial_fully_faithful_1cell : fully_faithful_1cell f. Proof. use make_fully_faithful. - exact from_biinitial_faithful_1cell. - intros z g₁ g₂ αf. assert(Hz : is_biinitial z). { exact (equiv_to_biinitial Hx (Sx z g₁)). } simple refine (_ ,, _). + apply (is_biinitial_2cell_property Hz). + apply (is_biinitial_eq_property Hz). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Examples.OpCellBicat. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Morphisms.FullyFaithful. Require Import UniMath.Bicategories.Morphisms.DiscreteMorphisms. Require Import UniMath.Bicategories.Morphisms.InternalStreetFibration. Require Import UniMath.Bicategories.Morphisms.InternalStreetOpFibration. Require Import UniMath.Bicategories.Colimits.Initial. Section FromInitial. End FromInitial.