Dan Friedman and David Christiansen recently published an introduction to dependent types, "The Little Typer". I attended Dan Christiansen's workshop, which drew on similar material, at the Code Mesh conference last year so I'm confident that this book will be fantastic to read.
We're organising a regular study group to read "The Little Typer".
In the third session we plan to discuss problems and points of interest from the third chapter of "The Little Typer". We'll use discussion happening in our forum* as the basis for face-to-face discussions.
If you want to try to write some code in the session then bring along a laptop with the Racket environment installed (available from https://racket-lang.org).
*We have a forum where summaries of the sessions are posted and where discussion about the book's content happen. Even if you can't attend the face-to-face sessions but want to participate then please contact me directly to join this forum.
Several people replied to my meetup email earlier this month expressing interest. I've already added those people to the RSVP list. Unfortunately the venue hosting us has very limited capacity.