Definition Catlike_associator_is_iso ( a b c d : category ) : ∏ f g h, is_iso (Catlike_associator a b c d (make_catbinprod f (make_catbinprod g h))). Proof. intros f g h. apply functor_iso_if_pointwise_iso. intros oba. apply (identity_is_iso d). 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.