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/ArrowLoop (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, though I'm really not sure. `CoStrong` seems to require laziness so it seems like costrong and cochoice should be flipped.

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.