Skip to content

maybe an oversight in the monad axioms? #584

Description

@affeldt-aist

join_unit : forall a, join _ \; (M <$> unit a) = idmap;

should be:

join_unit : forall a, unit (M a) \; join _ = idmap;

moreover, what about the following renamings:

unit_join -> Munit_join
join_unit -> unitM_join

@t6s @shinya-katsumata

(we're enjoying cat.v very much anyway ^_^)

Metadata

Metadata

Assignees

No one assigned

    Labels

    questionFurther information is requested

    Type

    No type

    Fields

    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions