For people just tuning in wondering what the significance of this math is: I see this kind of research potentially may lead to new and powerful methods to deal with self-reflection & self-modification. At the moment, current tools are quite limited.
I’d be curious what your take on Benabou’s perspective is which sees fibrations as more fundamental than indexed categories and would probably bristle at trying to prove they’re ‘equal’/ equivalent.
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.
If I remember correctly Benabou points out that indexed categories correspond to split fibrations.
The splitting internally corresponds to a notion of equality.
The existence of a splitting for every fibration uses (is equivalent to?) the axiom of choice.
In my reading, Benabou seems to say something to the effect that in naive category theory (read ‘synthetically’) not all categories come with an equality, each such equality structure corresponds to a splitting of the fibration obtained by externalization.
Synthetics comes to LessWrong! Very cool.
For people just tuning in wondering what the significance of this math is: I see this kind of research potentially may lead to new and powerful methods to deal with self-reflection & self-modification. At the moment, current tools are quite limited.
I’d be curious what your take on Benabou’s perspective is which sees fibrations as more fundamental than indexed categories and would probably bristle at trying to prove they’re ‘equal’/ equivalent.
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.
If I remember correctly Benabou points out that indexed categories correspond to split fibrations. The splitting internally corresponds to a notion of equality. The existence of a splitting for every fibration uses (is equivalent to?) the axiom of choice. In my reading, Benabou seems to say something to the effect that in naive category theory (read ‘synthetically’) not all categories come with an equality, each such equality structure corresponds to a splitting of the fibration obtained by externalization.