Definition Catlike_pentagon ( a b c d e : category ) (hsB : has_homsets b) (hsC : has_homsets c) (hsD : has_homsets d) (hsE : has_homsets e) : ∏ k h g f, (Catlike_associator a b c e ) (make_catbinprod k (make_catbinprod h ((functorial_composition c d e ) (make_dirprod g f)))) · (Catlike_associator a c d e ) (make_catbinprod ((functorial_composition_legacy a b c) (make_dirprod k h)) (make_catbinprod g f)) = (functor_on_morphisms (functorial_composition_legacy a b e) (catbinprodmor (identity k) ((Catlike_associator b c d e) (make_catbinprod h (make_catbinprod g f)))) · (Catlike_associator a b d e ) (make_catbinprod k (make_catbinprod ((functorial_composition_legacy b c d ) (make_dirprod h g)) f))) · functor_on_morphisms (functorial_composition_legacy a d e ) (catbinprodmor ((Catlike_associator a b c d ) (make_catbinprod k (make_catbinprod h g))) (identity f)). Proof. intros k h g f. apply (nat_trans_eq hsE). 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.