proposition: Proposition REL_comonoid_to_lunit : islunit (pr2 REL_comonoid_to_setwithbinop) REL_comonoid_to_unit.
proof: Proof. intro X. use funextsec ; intro y ; cbn in y. use hPropUnivalence. - use factor_through_squash_hProp. intros ( x₁ & x₂ & p₁ & p₂ & p₃ ). unfold REL_comonoid_to_unit in p₁. assert (y = x₂) as q. { apply (eqweqmaphProp (eqtohomot (eqtohomot (comonoid_to_law_unit_left _ C) y) x₂)). cbn. use hinhpr. refine ((tt ,, x₂) ,, _ ,, idpath _). use hinhpr ; cbn. refine ((x₁ ,, x₂) ,, _) ; cbn. refine (p₃ ,, idpath _ ,, p₁). } rewrite q. exact p₂. - intro Hy. assert (q := eqweqmaphProp (!eqtohomot (eqtohomot (comonoid_to_law_unit_left _ C) y) y) (idpath _)). revert q. use factor_through_squash_hProp. intros [ [ [] a ] [ H p ] ] ; cbn in p. induction p. revert H. use factor_through_squash_hProp. intros [ [ b₁ b₂ ] [ q₁ [ q₂ q₃ ] ] ] ; cbn in q₁, q₂, q₃. induction q₂. use hinhpr. refine (b₁ ,, b₂ ,, _ ,, _ ,, _) ; cbn. + exact q₃. + exact Hy. + 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