Skip to content

refactoring and correction in examples/cat.v#587

Open
t6s wants to merge 1 commit intomath-comp:masterfrom
t6s:cat20260401
Open

refactoring and correction in examples/cat.v#587
t6s wants to merge 1 commit intomath-comp:masterfrom
t6s:cat20260401

Conversation

@t6s
Copy link
Copy Markdown
Member

@t6s t6s commented Apr 1, 2026

fix #583, #584, #585

  • make \o the primary notation and ; parsing only
  • change the comp axioms to be about comp, not seq
  • fix (co)monad laws and their names
  • add IsCat factory
  • add IsFunctor factory
  • add IsExtensionMonad factory

Co-authored-by: @affeldt-aist @shinya-katsumata

* make \o the primary notation and \; parsing only
* change the comp axioms to be about comp, not seq
* fix (co)monad laws and their names
* add IsCat factory
* add IsFunctor factory
* add IsExtensionMonad factory

Co-authored-by: @affeldt-aist @shinya-katsumata
@t6s t6s changed the title refactoring and correction refactoring and correction of examples/cat.v Apr 1, 2026
@t6s t6s changed the title refactoring and correction of examples/cat.v refactoring and correction in examples/cat.v Apr 1, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

PreCat_IsMonoidal -> PreCat_IsPreMonoidal?

1 participant