giraj

It's great that you're offering a mentorship program, but I would have been one of those students complaining. In a business setting I understand the need to optimize onboarding, but in an educational setting I think inclusiveness should rank higher.

In our student organizations (at university) we've settled on Teams, which is what's available through our university accounts. I'd guess most universities have an equivalent, but let me know if I'm wrong. This has the benefit of requiring no sign-up, and separating work and personal life.

If you're talking about HS students, then I'd be surprised to hear that they're unwilling to install your preferred chat app to join the program.

Yep! You could check this in GHCi (the repl), for example:

  > :t (. id)
  > (. id) :: (b -> c) -> b -> c

(:t prints the type of an expression, and id is the "identity function" that's b -> b here.)

(EDIT: Maybe you know the above and you're asking if it's being changed in the proposal. It doesn't seem so to me.)

Your indexing is off :) Propositions (or 'facts' as you call them) are the (-1)-types, whereas 0-types are usually referred to as sets. A way to remember this is that the path-spaces (i.e. equalities) in a set are propositions, bringing you one level down.

While you're right that "proof relevance" is one of the key features of HoTT, I don't agree that what's being described here "is the HoTT point of view". Any mathematical proof bears on techniques that may be interesting beyond the proven result itself; HoTT doesn't clarify or elucidate that, nor does it aim to.

Had a blast at LauzHack '16 using this library to make a Chrome extension enabling "no-hands scrolling"[1]. Sadly, reading web articles while eating with both hands is still a dream. We managed to get okay-ish results on a MacBook Pro in perfect lighting from time to time, but nothing consistent. In variable lighting and on lower-end laptops we found it impossible.

I wonder if it would be possible with a better webcam and good, consistent lighting.

[1] https://github.com/jarlg/lookmanohands

There is a lot of discussion concerning COVID-19 over at LessWrong that might fit your bill: https://www.lesswrong.com/tag/coronavirus

Another alternative is Melatonin[1] which tries to imitate f.lux for chrome(book) users.

[1] https://giraj.github.io/melatonin

Thank you for this one. I think it ties in nicely with the idea of "goal factoring" (also from LW) where you ask yourself "why am I doing what I do? Is there a more direct way of achieving this?" This can be helpful when working with habits and maintaining harmony between your goals and emotions.

I've been using Chromebook as only computer for the last year as a student/developer(/tech-entusiast) and I am very satisfied.

I have the Samsung ARM one, and I've installed chroagh[1] (super easy, run one command and you have an arch install) headless, so I have a complete linux terminal. SSH would also work.

Right now I'm looking to upgrade (to macbook air 11" I hope) for more power with the same 8h battery time.

As a mobile and disposable (cheap!) terminal (and browser!), I can definitely recommend a chromebook.

[1] https://github.com/drinkcat/chroagh