Skip to content

Instantly share code, notes, and snippets.

@masaeedu

masaeedu/gist:9c25b89594a2417f6668d2dd00fbcbba

Created March 10, 2020 05:02
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save masaeedu/9c25b89594a2417f6668d2dd00fbcbba to your computer and use it in GitHub Desktop.
Save masaeedu/9c25b89594a2417f6668d2dd00fbcbba to your computer and use it in GitHub Desktop.
Download ZIP
Applicative right unit via natural isomorphism
Raw
gistfile1.txt
zipr = tabulate . zipf . bimap index index
huskr = tabulate . huskf
Right unit law
---
map2 huskr > zipr > map runit_fwd
= {definitions}
map2 (tabulate < huskf) > (tabulate < zipf < bimap index index) > map runit_fwd
= {syntax}
map2 (huskf > tabulate) > bimap index index > zipf > tabulate > map runit_fwd
= {functor2}
map2 huskf > map2 tabulate > bimap index index > zipf > tabulate > map runit_fwd
= {naturality}
map2 huskf > map2 tabulate > map2 index > map1 index > zipf > tabulate > map runit_fwd
= {functor2}
map2 huskf > map2 (tabulate > index) > map1 index > zipf > tabulate > map runit_fwd
= {repiso}
map2 huskf > map2 id > map1 index > zipf > tabulate > map runit_fwd
= {functor1}
map2 huskf > id > map1 index > zipf > tabulate > map runit_fwd
= {category1}
map2 huskf > map1 index > zipf > tabulate > map runit_fwd
= {naturality}
map1 index > map2 huskf > zipf > tabulate > map runit_fwd
= {naturality}
map1 index > map2 huskf > zipf > map runit_fwd > tabulate
= {applicative3}
map1 index > runit_bwd > tabulate
= {idk what this is but it feels ok}
runit_bwd > index > tabulate
= {repiso}
runit_bwd > id
= {category1}
runit_bwd
---
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment