psuedobrain

`CoChoice` is defined in the Haskell profunctors package. If I had to make an unsubstantiated guess, I would say that CoChoice corresponds to cofixpoints/corecursion and CoStrong (not shown here but has type `((a, d) ~> (b, d)) -> (a ~> b)`) corresponds to fixpoints/recursion. Like yccs27 was saying, this would mean that cochoice corresponds to apomorphims and costrong corresponds to paramorphisms.

Slight nitpick, but isn't Agda based on the MLTT family instead of CoC family of languages?

I think the question of whether field lines are real is more of a philosophical (of physics) question so it usually falls outside the scope of introductory material on E&M. However, some texts like Purcell and Morin do kinda take a stance on whether fields are real: "since it works, it doesn’t make any difference."

am i the only one for which programming language textbooks, papers, blog posts, etc. in racket are really hard to follow? the fact that the languages that is being operated on often looks exactly like racket makes it really hard to separate the two if i wanted to follow the tutorials in any other language.

CEK[1] machines are very clean way of implementing continuations or other features that can be implemented in terms of them in a language with no support for lambdas or closures. they are also reasonably fast too. i implemented a simple unlambda[2] interpreter in haskell using the cek/cesk style and it was ~20% faster and more memory efficient than the fastest c interpreter i could find.

[1] https://matt.might.net/articles/cek-machines/ [2] http://www.madore.org/~david/programs/unlambda/