Lemma totalcategory_rightunitorisnatiso : rightunitor_is_natiso TruD. Proof. intros x. use tpair. + use tpair. - exact (pr1 (ruiso (pr1 x))). - set (pf := (((pr2 (pr1 (pr2(pr1 C)))) _ _) (pr1 (ruiso (pr1 x)))) ). admit. + use tpair. - use total2_paths_b. -- exact (pr1 (pr2 (ruiso (pr1 x)))). -- admit. - use total2_paths_b. -- exact (pr2 (pr2 (ruiso (pr1 x)))). -- admit. (* etrans. { apply mor_disp_transportf_postwhisker. } apply transportb_transpose_right. etrans. { apply transport_f_f. } etrans. { apply maponpaths. apply (pr1 (pr2 (druiso (pr1 x) (pr2 x)))). } etrans. { apply transport_f_f. } apply transportf_set. apply homset_property. 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.