I’ve recently started studying Topology, which turned out to be a topic filled with set theory and theorems around it. Unfortunately, my brain was well-poisoned with Type Theory by the time I’ve started, so I couldn’t help but itch my hands in an attempt of encoding things in Type Theory.