Lemma totalcategory_pentagonidentity : pentagon_identity TαD. Proof. intros w x y z. use total2_paths_b. + exact (pen (pr1 w) (pr1 x) (pr1 y) (pr1 z)). + exact (dpen (pr1 w) (pr1 x) (pr1 y) (pr1 z) (pr2 w) (pr2 x) (pr2 y) (pr2 z)). 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.Monoidal.AlternativeDefinitions.MonoidalCategoriesCurried. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.DisplayedMonoidalCurried. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsCurried. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Total.