Observational Equality Now (For Good?)

*** PLEASE NOTE THAT WE ARE MEETING ON SUNDAY, NOT SATURDAY ***

After much headbanging, I got Google's AI to explain observational equality to me. The tl;dr is don't use J.

Let's try diving a little deeper than that by attempting to wade through Alternkirch, McBride, and Swiestra's original 2007 paper Observational Equality, Now! (http://strictlypositive.org/obseqnow.pdf). If that paper proves too murky, maybe we can try to extract some clarity from the successor 2022 paper by Pujet and Tabareu Observational Equality: Now for Good (https://inria.hal.science/hal-03367052v4/document).

We'll meet over Zoom and post the meeting URL here a few minutes before meeting start time.