proposition: Proposition REL_comonoid_to_assoc : isassoc (pr2 REL_comonoid_to_setwithbinop).
proof: Proof. intros X Y Z. use funextsec ; intro y. use hPropUnivalence. - use factor_through_squash_hProp. intros ( a₁ & a₂ & H & p₁ & p₂ ). revert H. use factor_through_squash_hProp. intros ( b₁ & b₂ & q₁ & q₂ & q₃ ). pose (eqweqmaphProp (eqtohomot (eqtohomot (comonoid_to_law_assoc _ C) y) (b₁ ,, (b₂ ,, a₂)))) as H. cbn in H. assert (H' := H (hinhpr ((((b₁ ,, b₂) ,, a₂) ,, hinhpr ((a₁ ,, a₂) ,, p₂ ,, idpath _ ,, q₃) ,, idpath _ ,, idpath _ ,, idpath _)))). revert H'. use factor_through_squash_hProp. intros [ [ c₁ c₂ ] [ r₁ [ r₂ r₃ ] ] ] ; cbn in r₁, r₂, r₃. induction r₂. apply hinhpr. simple refine (c₁ ,, c₂ ,, q₁ ,, _ ,, _). + use hinhpr ; cbn. exact (b₂ ,, a₂ ,, q₂ ,, p₁ ,, r₃). + exact r₁. - use factor_through_squash_hProp. intros ( a₁ & a₂ & p₁ & H & p₂ ). revert H. use factor_through_squash_hProp. intros ( b₁ & b₂ & q₁ & q₂ & q₃ ). pose (eqweqmaphProp (!eqtohomot (eqtohomot (comonoid_to_law_assoc _ C) y) (a₁ ,, (b₁ ,, b₂)))) as H. assert (H' := H (hinhpr ((a₁ ,, a₂) ,, p₂ ,, idpath _ ,, q₃))). revert H'. use factor_through_squash_hProp. intros [ [ [ c₁ c₂ ] c₃ ] [ K [ r₁ [ r₂ r₃ ] ] ] ] ; cbn in r₁, r₂, r₃. revert K. use factor_through_squash_hProp. intros [ [ d₁ d₂ ] [ s₁ [ s₂ s₃ ] ] ] ; cbn in s₁, s₂, s₃. induction r₁, r₂, r₃, s₂. apply hinhpr. simple refine (d₁ ,, d₂ ,, _ ,, q₂ ,, s₁). apply hinhpr ; cbn. simple refine (c₁ ,, c₂ ,, p₁ ,, q₁ ,, _) ; cbn. exact s₃. 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