# orderedItems[].object.content
@jonmsterling Oh huh, I haven't heard much about stoups! I guess my motivations for this rule are that it seems clear from a pedagogical perspective, and that it doesn't actually seem to get in the way of the type theory at all. But I am thinking about it truly as a name, so thinking about this as essentially using a stoup might offer some neat insights! I'll have to look into them more.

# orderedItems[].object.contentMap.en
@jonmsterling Oh huh, I haven't heard much about stoups! I guess my motivations for this rule are that it seems clear from a pedagogical perspective, and that it doesn't actually seem to get in the way of the type theory at all. But I am thinking about it truly as a name, so thinking about this as essentially using a stoup might offer some neat insights! I'll have to look into them more.

# orderedItems[].object.content
@jonmsterling Yep! Except that in this case, the name of the variable of type A is forced to be x.1, which isn’t something that usually happens in type theory presentations.

# orderedItems[].object.contentMap.en
@jonmsterling Yep! Except that in this case, the name of the variable of type A is forced to be x.1, which isn’t something that usually happens in type theory presentations.

# orderedItems[].object.content
@chrisamaphone Oh cool! This gave off a lot of ominous vibes to the people I showed it to, so I’m glad it’s not actually that unusual :p Do you have a link to the sequent calculus thing by Frank? I tried searching for it a bit but came up empty. No worries if not though!

# orderedItems[].object.contentMap.en
@chrisamaphone Oh cool! This gave off a lot of ominous vibes to the people I showed it to, so I’m glad it’s not actually that unusual :p Do you have a link to the sequent calculus thing by Frank? I tried searching for it a bit but came up empty. No worries if not though!

# orderedItems[].object.content
@ahfrom I miss this :( subtitles are now required for me to understand anything being said in today's shows and movies

# orderedItems[].object.contentMap.en
@ahfrom I miss this :( subtitles are now required for me to understand anything being said in today's shows and movies

# orderedItems[].object.content
To be clear, this is meant to be read as a bottom-to-top backwards-reasoning rule. The vision I have is that these kinds of name constraints flow upwards, so there's never any issue with incompatible constraints. I think any left rule for negative types should be amenable to this kind of approach, including function application which might be even more cursed lmao.

# orderedItems[].object.contentMap.en
To be clear, this is meant to be read as a bottom-to-top backwards-reasoning rule. The vision I have is that these kinds of name constraints flow upwards, so there's never any issue with incompatible constraints. I think any left rule for negative types should be amenable to this kind of approach, including function application which might be even more cursed lmao.

# orderedItems[].object.content
Had a cursed idea for a type theory rule. Note that 𝑥.1 is the name of the variable of type A, not an expression!

Everyone I've shown this to has been uneasy about it lol, but I really like it! It simplifies terms while letting the variable rule/identity rule still be admissible. And I think pedagogically it's helpful!

# orderedItems[].object.contentMap.en
Had a cursed idea for a type theory rule. Note that 𝑥.1 is the name of the variable of type A, not an expression!

Everyone I've shown this to has been uneasy about it lol, but I really like it! It simplifies terms while letting the variable rule/identity rule still be admissible. And I think pedagogically it's helpful!

# orderedItems[].object.attachment[].name
Type Theory derivation rule that looks like the left first projection rule for products in sequent calculus, with the name of the variable of type A times B being x, except that the name of the variable of type A introduced in the context by the rule is forced to be x dot 1.

# orderedItems[].object.content
Update: The meds worked!!! Over the next few weeks I'll titrate up to stronger and stronger doses, but even at just the starting dose, last night felt like the best night of sleep I've had in a while!

I did wake up for like ten minutes four hours in feeling extremely energetic, but then the extended release dose hit and I got knocked out again lol. And I'm sure as the dosage increases that interim period will disappear. So all this is really good!! And it leaves me super hopeful for the future! :)

# orderedItems[].object.contentMap.en
Update: The meds worked!!! Over the next few weeks I'll titrate up to stronger and stronger doses, but even at just the starting dose, last night felt like the best night of sleep I've had in a while!

I did wake up for like ten minutes four hours in feeling extremely energetic, but then the extended release dose hit and I got knocked out again lol. And I'm sure as the dosage increases that interim period will disappear. So all this is really good!! And it leaves me super hopeful for the future! :)

# orderedItems[].object.content
Taking my first dose of Lumryz tonight!!! Hell of a road to get here, but it’s finally time. Wish me luck :) #Narcolepsy

# orderedItems[].object.contentMap.en
Taking my first dose of Lumryz tonight!!! Hell of a road to get here, but it’s finally time. Wish me luck :) #Narcolepsy

# orderedItems[].object.content
Eta-expansion is just proof-relevant identity-elimination.

# orderedItems[].object.contentMap.en
Eta-expansion is just proof-relevant identity-elimination.

# orderedItems[].object.content
@isAdisplayName Yeah exactly!! I feel like even the way I think about logic and mathematics as a whole changed as I started working in type theory more and more, and I feel like it's easier for me to "get" the structure of a proof now.

# orderedItems[].object.contentMap.en
@isAdisplayName Yeah exactly!! I feel like even the way I think about logic and mathematics as a whole changed as I started working in type theory more and more, and I feel like it's easier for me to "get" the structure of a proof now.

# orderedItems[].object.content
Had an interesting discussion today about the importance and role of terms when teaching students about proofs! Specifically in the context of proof assistants, that is.

This came about because for one of my projects I'm currently designing a proof assistant that's intended to help teach students proofs. And it was brought up that I need to consider if exposing students to terms at all in the proof assistant actually helps work towards the stated pedagogical goal.

Personally, I feel like I've benefited a lot from working in proof assistants like Agda that expose terms directly to the user, and that I have a much better mental model of how these tools work compared to more tactic-heavy proof assistants like Lean. And relatedly, I also feel like thinking about proofs and propositions through the lens of terms and types has benefited me even outside of working in proof assistants.

But there definitely is an argument to be have here, and it's one I haven't really been considering much until now. I kind of only recently figured that incorporating terms in a proof assistant would help students acclimate to existing proof assistants if they later started using them, so I was going to do so because of that, but I don't think that alone is a good enough reason now.

# orderedItems[].object.contentMap.en
Had an interesting discussion today about the importance and role of terms when teaching students about proofs! Specifically in the context of proof assistants, that is.

This came about because for one of my projects I'm currently designing a proof assistant that's intended to help teach students proofs. And it was brought up that I need to consider if exposing students to terms at all in the proof assistant actually helps work towards the stated pedagogical goal.

Personally, I feel like I've benefited a lot from working in proof assistants like Agda that expose terms directly to the user, and that I have a much better mental model of how these tools work compared to more tactic-heavy proof assistants like Lean. And relatedly, I also feel like thinking about proofs and propositions through the lens of terms and types has benefited me even outside of working in proof assistants.

But there definitely is an argument to be have here, and it's one I haven't really been considering much until now. I kind of only recently figured that incorporating terms in a proof assistant would help students acclimate to existing proof assistants if they later started using them, so I was going to do so because of that, but I don't think that alone is a good enough reason now.

# orderedItems[].object.content
Maybe we should stop writing terms and using them to construct derivation trees, and start constructing derivation trees and using them to read off terms.

# orderedItems[].object.contentMap.en
Maybe we should stop writing terms and using them to construct derivation trees, and start constructing derivation trees and using them to read off terms.

# orderedItems[].object.content
@amy Oof I still remember getting mine taken out :( hope the pain gets better soon and that you have a speedy recovery!

# orderedItems[].object.contentMap.en
@amy Oof I still remember getting mine taken out :( hope the pain gets better soon and that you have a speedy recovery!