Taking my position as HoTT sci-comm seriously, I feel like I should do a Twitter thread explaining this announcement:

groups.google.com/g/homotopytype…

Or, alternatively, why a bunch of really smart people are excited about getting a computer to print out -2. Strap in! 🧵 If you need a refresher, HoTT (homotopy type theory) is a foundational system for mathematics where the basic objects we manipulate are "homotopy types", that is, "topological spaces considered up to homotopy equivalence". The actual setup is a bit more general, but that's 2/

gonna be tweeting while I read "A type theory for synthetic ∞-categories" by Riehl and Shulman (arxiv:1705.07442). mute this thread if you don't want to see it, i guess second page and I'm already not clear on something — though it is just the introduction. first, context:

their interpretation of ∞-categories is going to take place in bisimplicial sets, i.e. presheaves over Δ^op × Δ^op. varying one interval gets the "spatial" structure,

What does an (∞,2)-topos look like from the inside. How do we make syntax for that. The groupoidal objects are just.. types, but what do the interesting categories look like? Complete Segal spaces? Certainly not some variety of cubical set, those have too much symmetry Can we axiomatise a directed interval object, pick out the simplices as ordered products of intervals, define the Segal maps, and say that an internal (∞,1)-category is one where those maps are equivalences — the normal type of equivalence?

amulet is so well designed, it's amazing (this tweet is sarcasm)

here are some objects/fams that are defined by an induction principle but are not the natural numbers

- empty type
- unit type
- booleans

parametrised:
- products
- coproducts
- lists
- all W-types

indexed:
- vectors
- finite sets
- equality

higher:
- quotients
- circle induction-recursion:
- tarski universes

induction-induction:
- [can't think of any]

higher induction-induction:
- the reals

everything is inductively defined except for dependent product types

@_c_perez Right, so, a type theory is a deductive system in which propositions are interpreted as "types" of mathematical objects. E.g., a proof of A ∧ B is a product of (a proof of A) × (a proof of B)

This is because products model the inference rules for conjunction: if you have an 1/? @_c_perez A and a B, you can put them together to make an A×B, and if you have an A×B, you can project out an A and a B

you can see this as an overgrown form of the Brouwer-Heyting-Kolmogorov interpretation

by the way did you know about the clip-path css property? here's how to make a square image into a squircle image: plt.abby.how/means/vw7H.html

and the result:
plt.abby.how/means/vw7H.html clip-path clips the contents of an element to a path, which can be one of the basic shapes (e.g. a circle) or it can be defined in regular old svg!

aaaaaaaaa i'm excited!! i'm excited I don't think I've been this happy in years
I could not be happier that they kept Super✭Affection as the opening

I'm so stupid for believing she actually cared about me lol no one does

I was talked into posting an "explanation" of type theory in the style of those annoying 🙄 twitter 🐦 threads 🧵, so:

Let's talk about type theory! 💖 Type Theory is the study of formal systems also called (confusingly 😵) *type theories*, but in a CS context, you're more likely to see them being called *type systems* 👩‍💻

They have applications in mathematics 🧮 and computer science 💻, so hopefully both camps can get into it!

also please someone explain adjunctions to me. i need to understand adjunctions to understand real-cohesive HoTT

eiyuu unmei no uta is my least favourite egoist song this is probably because, since i have a brain, fate/apocrypha is my least favourite nasuverse property