proposition: Proposition cofree_comonoid_REL_coassoc : cofree_comonoid_REL_comult · cofree_comonoid_REL_comult #⊗ identity _ · mon_lassociator _ _ _ = cofree_comonoid_REL_comult · identity _ #⊗ cofree_comonoid_REL_comult.
proof: Proof. use funextsec ; intro x. use funextsec ; intro y. induction y as [ y₁ [ y₂ y₃ ]]. use hPropUnivalence. - use factor_through_squash_hProp. intros H. induction H as [ [ [ a₁ a₂ ] a₃ ] [ H [ p₁ [ p₂ p₃ ] ] ] ] ; cbn in p₁, p₂, p₃. revert H. use factor_through_squash_hProp. intros H. induction H as [ [ b₁ b₂ ] [ q H ] ] ; cbn in q. revert H. use factor_through_squash_hProp. intros H. cbn in H. induction H as [ [ [ c₁ c₂ ] c₃ ] [ [ r₁ r₂ ] [ r₃ r₄ ] ] ] ; cbn in r₁, r₂, r₃, r₄. induction p₁, p₂, p₃, r₁, r₄. pose (r₅ := maponpaths dirprod_pr1 r₃) ; cbn in r₅. pose (r₆ := maponpaths dirprod_pr2 r₃) ; cbn in r₆. induction r₅, r₆. rewrite <- r₂ in q. assert (m (m c₁ c₂) b₂ = m c₁ (m c₂ b₂)) as s. { exact (assocax Mmonoid c₁ c₂ b₂). } rewrite s in q. refine (hinhpr _). refine ((c₁ ,, m c₂ b₂) ,, _). split. + exact q. + refine (hinhpr _). exact ((_ ,, _) ,, (idpath _ ,, idpath _) ,, (idpath _ ,, idpath _)). - use factor_through_squash_hProp. intros H. induction H as [ [ a₁ a₂ ] [ p H ]] ; cbn in p. revert H. use factor_through_squash_hProp. intros H. induction H as [ [ b₁ b₂ ] [ [ q₁ q₂ ] [ q₃ q₄ ]]] ; cbn in q₁, q₂, q₃, q₄. induction q₁, q₂, q₃. rewrite <- q₄ in p ; clear q₄. assert (m a₁ (m y₂ y₃) = m (m a₁ y₂) y₃) as s. { exact (!(assocax Mmonoid a₁ y₂ y₃)). } rewrite s in p. refine (hinhpr (((a₁ ,, y₂) ,, y₃) ,, _)). refine (_ ,, idpath _ ,, idpath _ ,, idpath _). refine (hinhpr ((m a₁ y₂ ,, y₃) ,, p ,, _)). refine (hinhpr _) ; cbn. simple refine (((a₁ ,, y₂) ,, y₃) ,, _) ; repeat split. 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