Definition enriched_eso_ff_orthogonal_factorization_system : orthogonal_factorization_system (bicat_of_enriched_cats V). Proof. use make_orthogonal_factorization_system. - exact enriched_eso_1cell. - exact enriched_ff_1cell. - intros. apply propproperty. - intros. apply propproperty. - exact (λ _ _ F, enriched_eso_ff_factorization F). - abstract (intros C₁ C₂ F G τ HF ; cbn ; use (essentially_surjective_nat_z_iso _ HF) ; exact (from_is_invertible_2cell_enriched _ τ)). - abstract (intros C₁ C₂ F G τ HF ; cbn ; exact (enriched_fully_faithful_invertible_2cell τ HF)). - intros B₁ B₂ C₁ C₂. exact enriched_eso_ff_orthogonal. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Subcategory.Core. Require Import UniMath.CategoryTheory.Subcategory.Full. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.ImageEnriched. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.DisplayedBicats.Examples.EnrichedCats. Require Import UniMath.Bicategories.OrthogonalFactorization.Orthogonality. Require Import UniMath.Bicategories.OrthogonalFactorization.FactorizationSystem.