proposition: Proposition cofree_comonoid_REL_map_counit : comonoid_counit REL_sym_mon_closed_cat C = cofree_comonoid_REL_underlying · comonoid_counit REL_sym_mon_closed_cat (cofree_comonoid_REL X).
proof: Proof. use funextsec ; intros x₁. use funextsec ; intros x₂. induction x₂. use hPropUnivalence. - intros y. refine (hinhpr (_ ,, _ ,, idpath _)). exact (eqweqmaphProp (!eqtohomot (monoidfununel (@free_abmonoid_extend X (REL_comonoid_to_monoid C) (λ c x, f x c))) x₁) y). - use factor_through_squash_hProp. intros [ a [ p₁ p₂ ]] ; cbn in p₁, p₂, a. apply (eqweqmaphProp (eqtohomot (monoidfununel (@free_abmonoid_extend X (REL_comonoid_to_monoid C) (λ c x, f x c))) x₁)). rewrite <- p₂. exact p₁. 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