Jason (jcreed) wrote,
Jason
jcreed
It was a day. Advisor meeting went okay. I am feeling less doomed for having, for all practical purposes, signed away my soul as a proof irrelevance monkey for some time the moment I started my senior thesis, since it really looks like an interesting corner of the whole logic-type-theory curry-howard tangle. It's not so much an exotic modality, I think, as just a way of sneaking equational theory in the back door. Or maybe it just captures what you really want when you do propositions-as-types, or as in Awodey and Bauer's paper title, propositions-as-[types]. Anyway, I feel pretty confident that it's something. Yeah.

But I have some stuff to chew on for a while, and I think I'll try to submit to TPHOLs for real this time around.

Not a terrible lot else going on. Went to classes, aleksey's talk, got roped into doing puzzlestorm saturday. Asked the algebraic topology prof if all groups arise as fundamental groups of some space (I thought they did) but he didn't know off-hand.
Subscribe

  • (no subject)

    More things to add to the "chord progressions that aren't cliches-I-already-know-about nonetheless covertly appearing in multiple places" file.…

  • (no subject)

    Consider the chord motion in Lights's "Cactus In The Valley" that happens around 49s in: v link goes here | F G C C | F G C C | F G Am D7 | F G…

  • (no subject)

    Cute little synth widget playground: https://blokdust.com/

  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    switch
    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    Help
  • 3 comments