juleshHoly shit I think the category of dependent lenses aka the category of containers aka the category of polynomial functors is cartesian closed and I completely missed it
To be fair the construction is gnarly as fuck (I can't figure out how to implement it in idris)
@julesh@mathstodon.xyz this, no?https://link.springer.com/chapter/10.1007/978-3-642-13962-8_2
I think Hyland calls it the Fundamental Theorem of Dependent Types
Martin Escardo@ohad@mathstodon.xyz @julesh@mathstodon.xyz
I am kind of tired of "fundamental theorem of <blah>".
I think the only fundamental one is that of calculus.
The so-called fundamental theorem of algebra doesn't use algebra to be proved, but instead analysis.
Vassil Nikolov | ΠΠ°ΡΠΈΠ» ΠΠΈΠΊΠΎΠ»ΠΎΠ²I propose these are all called
"fundamental theorem of mathematics <number>".
Say, in approximate chronological order of publication.
@MartinEscardo@mathstodon.xyz @ohad@mathstodon.xyz @julesh@mathstodon.xyz