The goal of this repository is to formalize the SSD paper (https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.3). It is supposed to act like the human-read version for formalization work that has been in parts done by an AI.

Matching to the paper:

• Definition 1.2 is called is-countable
• Definition 1.3 is called is-countably-presented
• Remark 1.4 is called is-countably-presented-equivalence