Definition enriched_fully_faithful_hom_iso (x y : C₁) : z_iso (C₂ ⦃ F x , F y ⦄) (C₂ ⦃ G x , G y ⦄). Proof. use make_z_iso. - exact (precomp_arr _ _ (τi x) · postcomp_arr _ _ (τc y)). - exact (precomp_arr _ _ (τc x) · postcomp_arr _ _ (τi y)). - split. + abstract (rewrite !assoc' ; rewrite (maponpaths (λ z, _ · z) (assoc _ _ _)) ; rewrite <- precomp_postcomp_arr ; rewrite !assoc' ; rewrite <- postcomp_arr_comp ; rewrite !assoc ; rewrite <- precomp_arr_comp ; rewrite !enriched_fully_faithful_iso_right ; rewrite precomp_arr_id ; rewrite postcomp_arr_id ; apply id_right). + abstract (rewrite !assoc' ; rewrite (maponpaths (λ z, _ · z) (assoc _ _ _)) ; rewrite <- precomp_postcomp_arr ; rewrite !assoc' ; rewrite <- postcomp_arr_comp ; rewrite !assoc ; rewrite <- precomp_arr_comp ; rewrite !enriched_fully_faithful_iso_left ; rewrite precomp_arr_id ; rewrite postcomp_arr_id ; apply id_right). 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.