proposition: Proposition ismonoidfun_comonoid_mor_REL_to_map : ismonoidfun comonoid_mor_REL_to_map.
proof: Proof. split. - intros y₁ y₂. use funextsec ; intro x. use hPropUnivalence. + intro z. assert (H := eqweqmaphProp (!eqtohomot (eqtohomot (underlying_comonoid_mor_comult φ) x) (y₁ ,, y₂)) (hinhpr (_ ,, z ,, idpath _))). revert H. 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₃. apply hinhpr. exact (a₁ ,, a₂ ,, q₂ ,, q₄ ,, p). + use factor_through_squash_hProp. intros ( a₁ & a₂ & p₁ & p₂ & p₃ ). assert (H := eqweqmaphProp (eqtohomot (eqtohomot (underlying_comonoid_mor_comult φ) x) (y₁ ,, y₂)) (hinhpr ((a₁ ,, a₂) ,, p₃ ,, hinhpr ((_ ,, _) ,, (idpath _ ,, p₁) ,, (idpath _ ,, p₂))))). revert H. use factor_through_squash_hProp. cbn. intros [ b [ q₁ q₂ ]]. rewrite <- q₂ in q₁. exact q₁. - use funextsec ; intro x. use hPropUnivalence. + intro z. exact (eqweqmaphProp (!eqtohomot (eqtohomot (underlying_comonoid_mor_counit φ) x) tt) (hinhpr (_ ,, z ,, idpath _))). + intro z ; cbn in z. assert (H := eqweqmaphProp (eqtohomot (eqtohomot (underlying_comonoid_mor_counit φ) x) tt) z). revert H. use factor_through_squash_hProp. intros [ a [ p q ]] ; cbn in q. rewrite q in 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