Definition eso_ff_orthogonal_factorization_system_bicat_of_univ_cats : orthogonal_factorization_system bicat_of_univ_cats. Proof. use eso_ff_orthogonal_factorization_system. - exact eso_ff_factorization_bicat_of_univ_cats. - exact univalent_cat_is_univalent_2_1. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.IsoCommaCategory. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.Examples.OneTypes. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Morphisms.Eso. Require Import UniMath.Bicategories.Morphisms.FullyFaithful. Require Import UniMath.Bicategories.Morphisms.Properties.ClosedUnderInvertibles. Require Import UniMath.Bicategories.Morphisms.Properties.EsoProperties. Require Import UniMath.Bicategories.Morphisms.Examples.MorphismsInOneTypes. Require Import UniMath.Bicategories.Morphisms.Examples.EsosInBicatOfUnivCats. Require Import UniMath.Bicategories.OrthogonalFactorization.Orthogonality. Require Import UniMath.Bicategories.OrthogonalFactorization.FactorizationSystem.