Lemma transported_comonoid_laws_unit_left : comonoid_laws_unit_left L (a,, transported_comonoid_data). Proof. unfold comonoid_laws_unit_left. cbn. unfold transported_comonoid_comult_data. etrans. { apply maponpaths_2. unfold transported_comonoid_counit_data. rewrite tensor_mor_right. rewrite tensor_comp_id_r. rewrite assoc. apply maponpaths_2. apply diagram_1. } etrans. { apply maponpaths_2. rewrite assoc'. apply maponpaths. apply tensor_swap'. } etrans. { rewrite assoc'. apply maponpaths. rewrite assoc'. apply maponpaths. apply tensor_lunitor. } etrans. { rewrite assoc'. apply maponpaths. rewrite ! assoc. apply maponpaths_2. rewrite <- tensor_mor_right. apply comonoid_to_law_unit_left. } 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.