Lemma transported_comonoid_laws_unit_right : comonoid_laws_unit_right L (a,, transported_comonoid_data). Proof. unfold comonoid_laws_unit_right. cbn. unfold transported_comonoid_comult_data. etrans. { apply maponpaths_2. unfold transported_comonoid_counit_data. rewrite tensor_mor_left. rewrite tensor_comp_id_l. rewrite assoc. apply maponpaths_2. apply diagram_2. } etrans. { apply maponpaths_2. rewrite assoc'. apply maponpaths. apply tensor_swap. } etrans. { rewrite assoc'. apply maponpaths. rewrite assoc'. apply maponpaths. apply tensor_runitor. } etrans. { rewrite assoc'. apply maponpaths. rewrite ! assoc. apply maponpaths_2. rewrite <- tensor_mor_left. apply comonoid_to_law_unit_right. } rewrite id_left. exact ir. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Comonoids.Category. Require Import UniMath.CategoryTheory.Retracts. Import ComonoidNotations.