proposition: Proposition cofree_comonoid_REL_map_comult : comonoid_comult REL_sym_mon_closed_cat C · cofree_comonoid_REL_underlying #⊗ cofree_comonoid_REL_underlying = cofree_comonoid_REL_underlying · comonoid_comult REL_sym_mon_closed_cat (cofree_comonoid_REL X).
proof: Proof. use funextsec ; intro y. use funextsec ; intros [ x₁ x₂ ] ; cbn in x₁, x₂. use hPropUnivalence. - use factor_through_squash_hProp. intros [ [ a₁ a₂ ] [ p H ] ]. revert H. use factor_through_squash_hProp. intros [ [ b₁ b₂ ] [ [ q₁ q₂ ] [ q₃ q₄ ] ] ] ; cbn in q₁, q₂, q₃, q₄. induction q₁, q₃. pose (eqweqmaphProp (!(eqtohomot (monoidfunmul (@free_abmonoid_extend X (REL_comonoid_to_monoid C) (λ c x, f x c)) b₁ x₂) y)) (hinhpr (a₁ ,, a₂ ,, q₂ ,, q₄ ,, p))) as q. apply hinhpr. exact (_ ,, q ,, idpath _). - use factor_through_squash_hProp. intros [ a [ p₁ p₂ ]] ; cbn in p₁, p₂. induction p₂. assert (H := eqweqmaphProp (eqtohomot (monoidfunmul (@free_abmonoid_extend X (REL_comonoid_to_monoid C) (λ c x, f x c)) x₁ x₂) y) p₁). revert H. use factor_through_squash_hProp. intros [ a₁ [ a₂ [ q₁ [ q₂ q₃ ] ] ] ] ; cbn in a₁, a₂, q₁, q₂, q₃. refine (hinhpr ((a₁ ,, a₂) ,, q₃ ,, _)). apply hinhpr ; cbn. simple refine ((x₁ ,, a₂) ,, (_ ,, _) ,, (_ ,, _)) ; cbn. + apply idpath. + exact q₁. + apply idpath. + exact q₂. 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