Definition Catlike_triangle ( a b c : category ) : ∏ f g, functor_on_morphisms (functorial_composition_legacy a b c) (catbinprodmor (identity f) (Catlike_left_unitor b c g)) = (Catlike_associator a b b c (make_catbinprod f (make_catbinprod (functor_identity b : [ _, _] ) g))) · functor_on_morphisms (functorial_composition_legacy a b c) (catbinprodmor (Catlike_right_unitor a b f) (identity g)). Proof. intros f g. apply (nat_trans_eq c). intros oba. simpl. unfold horcomp_data; simpl. repeat rewrite functor_id. repeat rewrite (id_left _). apply idpath. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Categories.StandardCategories. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.Bicategories.WkCatEnrichment.prebicategory.