Identity Systems as Effect Handlers

In the 1Lab, we use Identity Systems all over the place to get a nicer verison of Path Types. In a sense, we are treating things like the J Rule as an Algebraic Effect, but in the Haskell sense, where we thread down dictionaries.