(Jointly written by Astra Kolomatskaia and Mike Shulman)
This is part one of a three-part series of expository posts on our paper Displayed Type Theory and Semi-Simplicial Types. In this part, we motivate the problem of constructing SSTs and recap its history.
A Prospectus
There are different ways to describe the relationship between type theory and set theory, but one analogy views set theory as like machine code on a specific CPU architecture, and type theory as like a high level programming language. From this perspective, set theory has its place as a foundation because almost any structure that one thinks about can be encoded through a series of representation choices. However, since the underlying... (read 2737 more words →)
The degree to which one would see this as a major downside would be strongly correlated with the factors that cause one to start taking HRT. There is a popular TERF narrative that detransitioners universally realise that everything was a mistake and regret the physical changes. From observation, however, this is rare and, if there's any concrete concrete identifiable reason for detransition like "I found Jesus Christ", detransitioners tend to not express significant levels of distress about the fact that they experienced physical changes.
I need to read about Benabou's perspective more, but otherwise I think that indexing and dependent types is just a syntactic layer used to describe fibrations. I explain this for about 15min in this timestamp of a recent talk of mine: https://youtu.be/vLCvrXJDPys?si=wxgLc_AZGsQmh93G&t=869
The catch is that fibring (n+1)-simplices (n+2)-separate times over n-simplices is the wrong way to form the fibration. One instead wants to form the matching object of (n+1)-simplex boundaries as a limit of the previous dimension data and fibre over it once. If you watch that excerpt from the talk, then I translate how to go from the indexed type-theoretic definition to that of a fibration.