I only found Setzers slides on this yesterday after trying to figure this out as I haven't been keeping up on Agda. So this is basically "copattern" matching on

I only found Setzers slides on this yesterday after trying to figure this out as I haven't been keeping up on Agda. So this is basically "copattern" matching on record projections. Records/structs are then the dual of variants/emums where we name and type the the destructors instead of the constructors. Thank you for confirming it. Agda's syntax then is meant to mimick descendants of C a little bit with that dot. I'm still fuzzy but it seems like this can be directly translated into an underlying term rewriting system and would just work almost unmodified and all we've done is opened a second route for type checking terms based on orthogonal conditions? I'll have a look at the nested copatters paper as that probably answers my question. Thank for the resources. They seem much clearer than my search results. I wonder why people don't start explaining codata with records instead of coNats and coLists. The latter was confusing.