Lemma is_binat_trans_inv_from_binatiso {F G : bifunctor_data A B C} {α : binat_trans F G} (isiso: is_binatiso α) : is_binat_trans (inv_from_binatiso isiso). Proof. split. - intros ? ? ? ?. apply pathsinv0. apply (z_iso_inv_on_right _ _ _ (α a b1 ,, isiso a b1)). rewrite assoc. apply (z_iso_inv_on_left _ _ _ _ (α a b2 ,, isiso a b2)). apply pathsinv0, (pr12 α). - intros ? ? ? ?. apply pathsinv0. apply (z_iso_inv_on_right _ _ _ (α a1 b ,, isiso a1 b)). rewrite assoc. apply (z_iso_inv_on_left _ _ _ _ (α a2 b ,, isiso a2 b)). apply pathsinv0, (pr22 α). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import  UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.ProductCategory. Import BifunctorNotations. Import BifunctorNotations. Section FunctorsFromProductCategory. Import BifunctorNotations. End FunctorsFromProductCategory. Import BifunctorNotations. Import BifunctorNotations. Import BifunctorNotations.