You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
I have been learning things among type theory, ∞-category theory and (classical) galois theory.
I have a question now.
Does anyone know there is study for a concrete application of generalized galois theory to type system extension such as extensions of simply typed lambda calculus ?
Edit:
Self resolved:
Model Category might be seen as the one with Pi-types whose fibrations act like Galois theory.
And it does not seem popular to apply galois theory to Simply Typed Lambda Caluculus rather than to a modern type system.