proposition: Lemma transported_comonoid_laws_unit_left : comonoid_laws_unit_left L (a,, transported_comonoid_data).
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Comonoids.Category UniMath.CategoryTheory.Retracts