proposition: Proposition cofree_comonoid_REL_counit_left : cofree_comonoid_REL_comult · (cofree_comonoid_REL_counit #⊗ identity _) · mon_lunitor _ = identity _.
proof: Proof. use funextsec ; intro x. use funextsec ; intro y. use hPropUnivalence. - use factor_through_squash_hProp. intros H. induction H as [ [ [] a ] [ H p ] ] ; cbn in a, p. revert H. use factor_through_squash_hProp. intros H. induction H as [ [ b c ] [ q H ] ] ; cbn in q. revert H. use factor_through_squash_hProp. intros [ [ [] d ] [ [ r₁ r₂ ] [ r₃ r₄ ] ] ]. cbn in r₁, r₂, r₃, r₄ ; cbn. refine (!q @ _ @ p). rewrite <- r₄. rewrite <- r₁. rewrite r₂. apply (lunax Mmonoid). - intros p ; cbn in p. induction p. refine (hinhpr _). refine ((tt ,, x) ,, _). refine (_ ,, idpath _). refine (hinhpr _). refine ((z ,, x) ,, _ ,, _). + apply (lunax Mmonoid). + refine (hinhpr _). refine ((tt ,, x) ,, _) ; cbn. repeat split ; apply idpath. Qed.
imports: UniMath.MoreFoundations.All UniMath.Algebra.Monoids UniMath.Algebra.Free_Monoids_and_Groups UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Categories.Rel UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Monads.Comonads UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Functors UniMath.CategoryTheory.Monoidal.Adjunctions UniMath.CategoryTheory.Monoidal.FunctorCategories UniMath.CategoryTheory.Monoidal.Displayed.TotalMonoidal UniMath.CategoryTheory.Monoidal.Displayed.Symmetric UniMath.CategoryTheory.Monoidal.Structure.Cartesian UniMath.CategoryTheory.Monoidal.Structure.Symmetric UniMath.CategoryTheory.Monoidal.Structure.Closed UniMath.CategoryTheory.Monoidal.Comonoids.Category UniMath.CategoryTheory.Monoidal.Comonoids.Monoidal UniMath.CategoryTheory.Monoidal.Comonoids.Symmetric UniMath.CategoryTheory.Monoidal.Comonoids.CommComonoidsCartesian UniMath.CategoryTheory.Monoidal.Examples.Relations UniMath.Semantics.LinearLogic.LafontCategory