Ruslan Φ. Russoul

Inductive-Recursive Types, Generally

I write about inductive-recursive types here. "Generally" means "higher inductive-inductive-recursive" or "quotient inductive-inductive-recursive". This may sound quite gnarly, but fortunately the specification of signatures can be given with just a few type formers in an appropriate framework.

In particular, we'll have a theory of signatures which includes Mike Shulman's higher IR example.

Recommendations for getting started on Category Theory, from emilypi, in NE Scala Slack (#category-theory), 3/14/20:

Right, so let's just go through the branches and name the suggestions:

Pure Theory

Categories in Context by Riehl (Mid-Advanced): this book is concise, formal, and modern. It has a slight bias towards categorical homotopy theory, but has the most correct and relatively complete approach to understanding universal properties that I've seen in any book. This approach is the key to understanding most of the theory. The exercises in this book are 👍
Category Theory by Awodey (Beginner-Mid): This one was mentioned. It is a straightforward, classical approach to category theory with a bias towards categorical logic. Exercises are 👋
Categories for the Working Mathematician by MacLane (Mid-Advanced): the standard. Read this to complete your understanding. I would recommend this book for understanding Limits + Colimits and CCC's before Riehl if its your first r

Screen Quick Reference

Basic

Description	Command
Start a new session with session name	`screen -S <session_name>`
List running sessions / screens	`screen -ls`
Attach to a running session	`screen -x`
Attach to a running session with name	`screen -r`

Introduction

C-a == Ctrl-a
M-a == Alt-a

General

:q        close
:w        write/saves
:wa[!]    write/save all windows [force]
:wq       write/save and close