Definition of monads on precategories and categories (+ of whiskering and horizontal composition)#1018

Merged

EgbertRijke merged 11 commits intoUniMath:masterfrom GregorPercic:monad

Feb 6, 2024

+284

Commits on Jan 31, 2024

some initial fragments of the definition of a monad (code not yet working)
GregorPercic
committed

Commits on Feb 1, 2024

the definition of a monad completed, horizontal composition of natural transformations remains to be defined
GregorPercic
committed

Commits on Feb 2, 2024

defined horizontal composition in terms of basic whiskering, which remains to be defined
GregorPercic
committed
rewrote the definition of a monad on a precategory in terms of whiskering, which remains to be defined
GregorPercic
committed

Commits on Feb 3, 2024

Commits on Feb 4, 2024

Commits on Feb 5, 2024

modified the explanation of horizontal composition to better fit its formal definition in the code, and also added some links
GregorPercic
committed

Commits on Feb 6, 2024

Merge branch 'master' into monad
EgbertRijke
authored