01-31 Friday
As this is my first weeknote, I must start by saying that I’ve been studying “SOGATs by example” for the last few weeks. At the time of writing this, I am stuck on exercise 37 which asks for a presyntax (minimal untyped AST) for Simply Typed Combinator Calculus, so that type inference always works. At first I got a strong reaction reading “untyped” (which made me think that I need to figure out a theory devoid of all types, but) I saw that there is a need of having types as information in the AST, while resulting to an untyped model overall. I have to flesh out the details on this…
Nonetheless, I had a bit of fun with CC; I figured out doubling (SII), which lead to an entertaining hunt for the fixed point combinator Y, on the way of figuring out how to do arithmetic in SK.
I have to admit, computation without variables is a fascinating concept (SK combinators are Turing complete).
Weekend
I’ve been a part of a Cubical Agda for about a month, and this time around I got to work on Exercises Session 8 (HoTTEST Seminar 2022). The last one in particular asks for a proof that contractibility is a proposition. I think I see the cube needed1 but I struggle with matching the boundary conditions on a particular edge. When I attempt to fix it, another one becomes problematic, leading to a circular chase of conditions-to-be-met.
Footnotes
-
I plan to add some explanatory and postscriptum-y drawings to make this clearer, ideally before anyone reads this. ↩