gistfile1.txt

Associativity:

(T :.: T :.: T) a
  \   /     /
   join    /
     \    /
      join  ===> T a    ---
                          |
                          |
                          |
(T :.: T :.: T) a         Must be the same
  \     \   /             |
    \     join            |
     \    /               |
      join  ===> T a    ---
      
      
Left identity:

If this layer is introduced via ⌜return⌝, then
 |
 |
 v
(T :.: T) a  ----------|
  \   /                Must be the same
   join   ===> T a  ---|
   
   
   
Right identity:

If this layer is introduced via ⌜return⌝, then
       |
       |
       v
(T :.: T) a  ----------|
  \   /                Must be the same
   join   ===> T a  ---|