"category theory was a mistake"

>>8409121
Damn fuckin right it was. Categories are dumb. Sets are all we need?

I have a set.
I have a set
Uhh
set of the sets given by the axiom of pairing

File: 1473789739802.gif (208KB, 354x534px) Image search: [Google]

208KB, 354x534px

There are no mistakes, only happy accidents.

>Be my friend
>Specialize in category theory
>Instantly become an expert since there are like 100 people in the field worldwide
>???
>Profit

File: Lurie looks down at you.jpg (153KB, 800x1200px) Image search: [Google]

153KB, 800x1200px

>>8409121
Only fringe people will forbid you to use sets, they form an important category.

>>8409726
Bullshit. "Category theory" in-of-itself is exhausted in MacLanes book. Say when you've set up adjoints. But that's like saying writing in-of-itself is exhausted once you consider all combinations of letters, making for words.
But to even understand the algebra and topology as written down by this prominent bloke
https://en.wikipedia.org/wiki/Jacob_Lurie
you need a shitton of working knowledge with category theory and there are much more than 100 people following work along his lines alone.

File: dont save this or else.png (1MB, 800x933px) Image search: [Google]

1MB, 800x933px

>mfw reading that the american air force funded category theory until they realized it wouldn't help build better killing machines

>>8409744
citation requested?

File: Capture.png (83KB, 515x530px) Image search: [Google]

83KB, 515x530px

>>8409747
mac lane's autobiography

>>.8409752
thx

>>8409744
>>8409747
Also, the nLab is funded by the Air Force. Read the home page.

File: 7823245.jpg (45KB, 372x246px) Image search: [Google]

45KB, 372x246px

>>8409121
>>8409133
>"Dude, what if everything is made of sets?"
>"Nah man, what if everything is made of arrows?"

File: pepe17.jpg (76KB, 653x590px) Image search: [Google]

76KB, 653x590px

>>8409783
>nLab is funded by the Air Force
how did the category theorists trick them again? what does the air force get out of nlab?

>>8409790
We constructed a localization between the category of funding and the category of fields, and because the inclusion functor reflects limits, we were able to show them that the limit to how much they would fund us didn't actually exist. They couldn't argue the facts!

File: Screen Shot 2016-10-13 at 15.47.34.png (64KB, 425x425px) Image search: [Google]

64KB, 425x425px

>>8409784
The philosophical point is that categories capture theories structually, i.e. everything UP TO invertible ARROWS in your category. Things in category theory aren't made of anything.
Set theoretical natural numbers are bunch of things 1,2,3,4, making for a collection N, so that you can define a function 'next' this takes you from one to the next. Cateogry theoretical natural numbers are the diagrams which for which the arrows around a particular arrow behave like 'next'.
And there is the cateogry of sets where of course the set N and its 'next' is a good example for that property.
There isn't one particular N in category theory, you can set up a category and ask if it has one or more natural number object or if it doesn't. An N there isn't necessarily make up of anything and a 'next' ('s' in the picture) is some arrow that was there all along.

File: 7y9yu9958.png (1MB, 1080x1920px) Image search: [Google]

1MB, 1080x1920px

>>8409802
They want battlefields, but they prefer these fields non-local. Some category theorist promised he would transfer projectiles away from local objects to the battlefields in another realm. Little did the warlords know the projectiles were not arrows in the martial sense.

There was a plane in the CAPTCHA... They know I know!

>>8409802
>>8409810
I'm glad you're having fun folks, but try to keep some credibility

>>8409810
Careful animenon, we mustn't start a conspiracy theory!

File: 46888.png (413KB, 849x480px) Image search: [Google]

413KB, 849x480px

>>8409830
The truth must be told.

File: 1476223377542.jpg (2MB, 3000x3000px) Image search: [Google]

2MB, 3000x3000px

>>8409956
will the most radical 21st century scripture be written in categorical notions?

File: 1463453053058.png (103KB, 264x299px) Image search: [Google]

103KB, 264x299px

>>8409960
It could be so. One could argue that the Germanic rune tiwaz itself is a category theoretical arrow symbol, and so it could be that this scripture is neo-paganic radicalism.

Someone give me a brief explanation of the fundamentals of catagory theory.

File: gon3.gif (592KB, 500x283px) Image search: [Google]

592KB, 500x283px

>>8409979
then consider me functorised

File: 1463261800572.png (568KB, 852x880px) Image search: [Google]

568KB, 852x880px

>>8409985
It is generalizing and abstracting familiar notions: one tries to define a universal property to familiar repeating structures, one generalizes set theoretical, algebraic, topological, etc. properties, one proves properties for the category theordtical notions which are then true for their realizations in a given category.

For every category, there is a class of its objects, a class of arrows from an object to another for any two objects in the category, and a binary operation amongst all the arrows called the composition. These are required to satisfy certain conditions, and the basic structure of a category stems from this. Between categories one can define functors which act as sort of homomorphisms. They have a lot of use, for example the homotopy, homology and cohomology functors in algebraic topology, or the functors taking groups, rings, algebras, etc. to their underlying sets and homomorphisms to simply functions between these sets. Topological groups are also born from changing the category for the underlying objects from sets to topological spaces.

There's something. Someone else would point in a totally different direction.

>>8409991
Nice.

File: Cm615zsWcAAUD9m.jpg (45KB, 960x659px) Image search: [Google]

45KB, 960x659px

>say something about category theory
>it turns into an anime thread

every time

>>8410051
So you just organize things?

File: pence2.png (148KB, 193x321px) Image search: [Google]

148KB, 193x321px

>>8410105
there's a reason why it's every autist's favourite branch of math

>>8410105
not op.

You could look at it that way, but that would be very misleading. set theory "just organizes" too. But the organization leads to proofs or statements otherwise difficult to prove or state at all.

eg: universal algebra has "free algebras", usually stated in terms of building up strings or trees and quotienting out by equalities induced by some axioms. This is not the most straightforward thing to state or generalize, and the important point really is that the free algebra has an initial property.

This initial property is straightforward to state with category theory, which makes generalizing freeness almost "automatic". Given a category C and a faithful functor U from C to Set, there is a free C-object for every set X iff U has a left adjoint.

In fact, we can generalize the situation: we can think of C as "concrete over D" by equipping it with any faithful functor U: C->D, and similarly say that if U has a left adjoint F, then F(d) is the free C-object generated by D. The fairly nasty universal algebra definition comes out automatically as a special case.

eg: in what sense are the two encodings of the cartesian product {{a},{a,b}} and {a,{a,b}} "the same"? Categorically this is easy - they are both an adjoint of the diagonal functor taking a set X to the pair of sets (X,X), and adjoints are always isomorphic.

"the" functorial example: for any pair of spaces X,Y, a continuous function from X to Y induces a group homomorphism from the ith homology group of X to the ith homology group of Y. This is just the statement that taking the ith homology group is functorial.

eg: finite dist lattices and finite posets are in correspondence - to each FDL we associate a poset of prime filters, and to each poset its open sets. However, the two collections are not "isomorphic". eg, any one-element FDL will correspond to the empty partial order. However, FDL^op is equivalent to FPoset, where "equivalence" simply means there are certain natural isomorphisms.

File: 1475807188218.jpg (1MB, 1154x1500px) Image search: [Google]

1MB, 1154x1500px

>>8409121
Functor? I 'ardly knew 'er!

>>8409806
>Things in category theory aren't made of anything.

This is actually a shortcoming of category theory. To actually construct anything (e.g. some construction like categories-in-C) you need to say what it's made of. Type theory subverts it to some degree, but the idea of exclusively focusing on external structure and not internal structure is very myopic. In fact there should be some duality between the two.

The real value in it is that you don't have to introduce any more structure than is needed by shoehorning everything into the cumulative hierarchy. Univalence makes this precise.

>>8410051
>For every category, there is a class of its objects, a class of arrows from an object to another for any two objects in the category, and a binary operation amongst all the arrows called the composition. These are required to satisfy certain conditions, and the basic structure of a category stems from this. Between categories one can define functors which act as sort of homomorphisms. They have a lot of use, for example the homotopy, homology and cohomology functors in algebraic topology, or the functors taking groups, rings, algebras, etc. to their underlying sets and homomorphisms to simply functions between these sets. Topological groups are also born from changing the category for the underlying objects from sets to topological spaces.

What a fucking terrible explanation. I hope you don't have to teach some freshman calculus class, you would just sperg out and start acting like an anime girl or something.

>>8409985

Categories generally represent some class of structures, and the morphisms (mappings) in the category preserve this structure. In particular, we say that A and B are isomorphic when there are morphisms f: A -> B, g: B -> A such that gf = 1 = fg. This means that instead of just saying things are "the same", you can also say exactly how they are the same (where "how" means by what isomorphism). So categories where all morphisms are invertible (groupoids) can be seen as generalizations of equivalence relations. General categories can thus be seen as generalizations of preorders, in that two things can be more than just related or not-related, there can be multiple "witnesses" to the relation between them.

File: gorilla.jpg (18KB, 222x258px) Image search: [Google]

18KB, 222x258px

>>8410066

even physics threads aren't this bad. category theory must be an autisto-super-attractor

File: baez.jpg (46KB, 445x442px) Image search: [Google]

46KB, 445x442px

>>8410751
Please don't take animu-man as being representative of the field. Most category theorists are quite sane and personable, like John Baez.

>>8409121
Today my prof said
>Anything that mathematics deals with is always some topological space together with a sheaf of rings
Is this autism?

>>8410803
yes

see combinatorics

>>8410803
Probably a fucking algebraic geometer, they think the whole universe revolves around their field. Some generalization of what he says might be true though.

>>8410806
to be fair:
this holds true for algebraic geometry, differential geometry, complex analysis, and even logic can be in many ways seen as a form of ring theory (re: joyal's "toposes are just rings")

>>8410066
>don't say something about category theory
>attention whore and his buttbuddy barge in and start jacking off over functors anyway
every time

>>8410751
>>8411035

i wasn't implyign that it's a bad thing
sure, they have shitty, entry-level taste in anime, but they're legitimately smart people talking about legitimate category theory

compare this to your seven daily gorilla posters who make threads like "if vegetables are good for you then why do they taste bad"

i don't like avatarfagging of any kind, but i much prefer it over retards complaining about how calculus is too hard

>>8411048
desu if we're going to start ranking cancer, I'll take 4chan cancer (shitpost) over reddit cancer (attention-whoring) any day

half their posts are blogshit anyway

File: 1397267528423.gif (2MB, 600x750px) Image search: [Google]

2MB, 600x750px

>>8409121

"My child was a mistake" -OP's mom

>>8409738
>This is what retards actually think.
10/10 lol, please kill yourself moron.

>>8410442
They are dual in a formal sense, a la Lawvere's work on the syntax-semantics adjunction. I have yet to come across a situation where I wish I had more intrinsic structure to fiddle with, but that is because I am very conditioned at this point to identify the external clockwork that I need to tweak or specify to affect what would be internal structure. Probably the biggest issue is when people work in enriched categories but try to work in the set-enriched manifestation. For example, working categorically with abelian groups is going to be really underpowered if you don't acknowledge the Ab enrichment. In a sense, it is "immoral" to forget this, just how it is immoral to forget about higher cells (this is why Top doesn't seem as nice as it is, since it lives most comfortably as an (∞,1)-category).

>>8411054
agreed

>>8411009
>toposes are just rings

This is going to take a lot more justification before resembling anything like a non-retarded statement.

>>8411374
>They are dual in a formal sense, a la Lawvere's work on the syntax-semantics adjunction.

It's not clear to me that this formalizes the exact concept I'm talking about, but it's definitely a step in the right direction.

>For example, working categorically with abelian groups is going to be really underpowered if you don't acknowledge the Ab enrichment. In a sense, it is "immoral" to forget this

How would you "forget" that?

Quant here. Curious as to how category theory will improve my earnings. Feel free to enlighten me. So far category and set theory look like a big classification gimmick. Jargon always impresses people.

>>8411475

also would like to know what important problems category theory is needed to solve. it was once said (ironically enough ) by a famous set theorist to his student while working on his thesis, "you can't solve a problem by inventing new formalism". what does category theory solve outside of category theory?

>>8411374
Just the other day I was asking you how an adjoint of some objects/sets etc. Could take you to a solution of a ODE and now you are under the impression you don't really have to look at elements??

Anyway, the issue of not looking at elements is one of the reasons people start to look at overcategories, where e.g. the objects are the arrows of the previous categories - then they set up functors to move between them, produce incomprehensible structures doing it and in the end claim that's an insight. That topoi sort of fizzled is justified I think

>>8411481
You can view it as a language to talk about static type systems - look up certified code.
(And hardly any field improves your earnings, pure math should be viewed like making msic anyway - for better or worse, music that you can't hear just by having ears, you must invest and care first)

>>8411481
>what important problems category theory is needed to solve

Fermat's Last Theorem, the abc conjecture, the Weil conjectures, and probably nearly every other big open problem out there outside of analysis.

>Anyway, the issue of not looking at elements is one of the reasons people start to look at overcategories, where e.g. the objects are the arrows of the previous categories

You're right it's accomplishing a similar thing, but it's actually a lot nicer than the ZFC way. It's only "incomprehensible" if you're a noob.

>That topoi sort of fizzled is justified I think

Dude, no. Topoi have basically been "figured out" but people have moved on to other areas of categorical logic like [math]\infty[/math]-topoi and quantum logic.

>>8411508
Been figured out without impace on pre 1940 problems

File: XpMBUZb.png (1MB, 1920x1080px) Image search: [Google]

1MB, 1920x1080px

>>8410466
>What a fucking terrible explanation. I hope you don't have to teach some freshman calculus class, you would just sperg out and start acting like an anime girl or something.
Haha, I admit that explanation sucks. I haven't taught high schoolers calculus, and maybe never will.

>>8410784
Animu-man is an algebraic topologist and homological algebraist. Misfielding me is very triggering!!

>>8411610
>Animu-man is an algebraic topologist and homological algebraist

They can have you, but the point still stands.

>not being a suave motherfucker like picrelated

File: jpetermay.gif (50KB, 286x239px) Image search: [Google]

50KB, 286x239px

>>8411630
shit, forgot pic

File: 6965562.jpg (635KB, 1920x1080px) Image search: [Google]

635KB, 1920x1080px

>>8411630
>>8411631
The point indeed stands. I have no intention or reason to even try denying it. I've been spamming about categories because of a project of mine is strongly related to category theory, and [math]\textbf{Cat}[/math] is a cute category!

>>8411468
http://youtu.be/Ro8KoFFdtS4
lecture series where joyal makes the claim

one presentation of a topos is saying that it has all colimits ("sums") which are preserved under certain pullback ("distributive property"). obv he really means something closer to frames, but the analogy is there and many techniques are formally similar. lots of people have borrowed terminology and proof methods from comm algebra for topoi.

Mathematical Physics grad student here who got conned into taking category theory and homological algebra. Are there any more applied style problems or structures that benefit from category theory?

As of right now I seem to be firmly working in the realms of abstract algebra and outside of Lie theory and small amounts of Algebraic Geom I never use algebra and I currently want to blow my brains out most lectures.

Is there light at the end of this tunnel? Even my supervisor said I don't really need to know any more Alg Geo so its not even useful for that.

>>8411488
The point is that you can view elements as arrows into the thing (global elements). I am not saying that an object should not be examined internal to itself, but rather that everything about that object up to isomorphism ought to be described in terms of arrows. This is true for solutions to differential equations in synthetic differential geometry, where they arise as lifting problems (equivalently, as connectivity problems in an overcategory, as you mentioned).

>>8411468
It's not a matter of literally forgetting it, but what I mean is that the internal language in Ab as a normal Set-enriched category is weaker than the internal language in Ab as an Ab-enriched closed monoidal category ("forgetting" monoidal structure is in the same vein).

File: 1476274837007.gif (636KB, 500x282px) Image search: [Google]

636KB, 500x282px

>>8411728
Use what you know about homological algebra to get a solid understanding of de Rham cohomology, and apply this to physics via differential geometry.

>>8411683
cool, will check it out

>>8411035
They make me cringe, too

File: 14641785.jpg (67KB, 600x928px) Image search: [Google]

67KB, 600x928px

why is it the case that the only real science and math which ever occurs here is either meme-y or highschool tier? When was the last time you saw actual math on sci which wasn't category theoretic tier memery? When was the last time you saw actual physics on sci which wasn't neckbeards jerking to manifestly covariant electrodynamics?

at this point the only redeeming quality sci possesses is the ease with which you can bait autists with pictures of pensive gorillas.

>>8413430
I love you gorilla-posters and your silly threads.

On a serious note, a while ago I tried to discuss open problems in Topology and set-theory, but nobody replied to me.

File: Kaffee-Filter.jpg (23KB, 640x483px) Image search: [Google]

23KB, 640x483px

>>8413438
just try it again, someone will reply eventually

>>8413430
If people want to discuss other topics, they ought to start threads. Are you out there, starting discussions on topics you are interested in? We are only responsible for discussing things we know or care about.

File: 1468572701135.jpg (50KB, 552x615px) Image search: [Google]

50KB, 552x615px

>>8413430
>calling category theory a meme

it is you who are the meme, anon

>>8413430
People don't want to invest time if they don't see their opposites, especially if you don't even know if anybody will reply. The quality of discussion on physics for non-babby staff is bad even on StackExchange physics.
Similarly, you can't expect to ask a real question on functional analysis or stochastics or whatever and expect an elaborate answer. There are not many specialists.
Category theory and the like is a high-effort-for-entrance subject and so you got some people who just learned it and some who want to learn and then people discuss. All the cateogry theory questions on /sci/ are also questions that you can ask after 3 weeks of learning the subject and the algebraic topology questions are question you'd ask after reading the nLab for 3 months.

>>8414117
This hits the nail on the head. It's still good to have an environment for initiates to ask questions and have discussions. That's a very important part of the learning process I think.

File: 1474948707550.png (208KB, 481x560px) Image search: [Google]

208KB, 481x560px

My mom had printed me Johnstone's Topos Theory. I am the [math]\infty[/math]-male!

>>8414780

topos theory? you ever get the feeling that this sort of thing is what Einstein referred to when he spoke of "more or less dispensable erudition"?

that sort of metamathematics is to mathematics what post modern critical theory is to social discourse; a virus.

>>8415397
being this butthurt

File: pepe18.jpg (59KB, 500x499px) Image search: [Google]

59KB, 500x499px

>>8415397
>category theory? you ever get the feeling that this sort of thing is what Einstein referred to when he spoke of "more or less dispensable erudition"?
t. someone 70 years ago

>>8411728
>8411728
nah, physicists, even more clearly graduates, are always at least 50 years behind mathematicians.

CT in physics is still an oddity. If you want to pursue CT, you must do it because you wonder what a formalization of space [as in 3d space].

Currently, you can use CT/topos theory in physics for
-QM, where the kochen specker theorem has a natural meaning, see isham, doering
this deals with algebraic QM/QFT through gelfand spectra
-some rewriting of field theory, from the guy from the nlab or from baez or from Zafiris and Mallios
-the work of lawvere himself on nlab
https://ncatlab.org/nlab/show/William+Lawvere
-In GR with the attempt to use domains to get GR with Panangaden


you must recall that when you use CT, you can work in classical math, in intuitionist math [powerset of a set exists] or in constructive math [not always a powerset of a set exists].

if you want to read about CT, read

From a Geometrical
Point of View
A Study of the History and Philosophy
of Category Theory
by
Jean-Pierre Marquis

>>8415444
>>8415444
>QM

Abramsky and Coecke deserve to be mentioned here.

>>8415444
>you must recall that when you use CT, you can work in classical math, in intuitionist math [powerset of a set exists] or in constructive math [not always a powerset of a set exists].

Huh? I guess by intuitionist math you mean topos theory. What do you mean by constructive math though?

>>8415508
constructive=constructive predicative=typically the the logic preserved by geometric functors, instead of the logical functors

>>8415500#
indeed. does coekce heve a breakthrough with his formalism?

>>8415712
What counts as a breakthrough to you? Most recently Coecke and Vicary have shown that orthogonal bases are the same as commutative dagger-Frobenius monoids.

>>8415715
yeah this. it was a big result. But there is still missing a result to show other physicists that category theory is useful to them.

>>8409121
Yeah what the hell is category theory even besides drawing some fancy arrows?

>>8415717
True, it's still in an exploratory phase I think. I guess the basic fact that Cob and Vect are both dagger categories (a la Baez's Quantum Quandaries: http://math.ucr.edu/home/baez/treilles/) is more likely to convince a physicist that category theory might be good for something rather than any particular result obtained so far.

>>8415723
>>8410466

>>8411728
Well Moduli Problems are important in String Theory. They are all Stacky and stuff.

File: Screen Shot 2016-10-16 at 14.10.48.png (102KB, 629x299px) Image search: [Google]

102KB, 629x299px

>>8414254
Ya, Thanks.

Speaking of which, I'm still going to do the Idris reading. Currently looking around for people to join

Speaking of which, approaching Univalence and it's contructive meaning,
looks like Coq-uand and the gang are trying to set up smaller systems where it holds.

https://arxiv.org/pdf/1610.00026v1.pdf

>>8414780
You're just flamboyant.

>>8415397
Topos theory can capture a lot of math faithfully, in an abstract and cumbersome language. Critical theory, or any philosophical framework, doesn't capture another subject 1:1 in terms of their propositions.

>>8415444
Do you have a concise paper or whatever where it's pointed out where intuitionist logic jumps off constructive logic? (Probably it's in Matrin Löfs texts, but is there something more to the point?)

>>8415717
>>8415730
As a physicist, let me tell you that the people using category theory aren't approaching any issues that would convince physicist, on a broad scale, of categories. In fact, I'm pretty sure there's nothing to gain in high energy physics in the next decade, and the QM questions could be called "non-problems". Their resolutions wont solve anyhting that's more interesting than any problem in turbulence.

>>8415866
>As a physicist, let me tell you that the people using category theory aren't approaching any issues that would convince physicist, on a broad scale, of categories.

Of course. New math is used to express concepts that you can't express in the old language, so it's only going to be interesting to people who are re-examining the conceptual foundations of physics...until it is made part of the standard toolkit by whoever uses it to construct the next theory. Remember that group theory was once considered cancerous by physicists; now everyone uses it.

File: Screen Shot 2016-10-16 at 16.00.53.png (120KB, 966x362px) Image search: [Google]

120KB, 966x362px

>>8415943
heh, they tell that story at the beginning of
http://www.springer.com/de/book/9783642128202
And you're right.
My quest is finding a problem that's of actual interest and approachable. It's the hope and dream of people that if you learn enough comfy math, like Cartesian closed categories are comfy, that you then come across a good problem that you then happen to be equipped to solve. Too romantic if you ask me.

>>8415950
>My quest is finding a problem that's of actual interest and approachable. It's the hope and dream of people that if you learn enough comfy math, like Cartesian closed categories are comfy, that you then come across a good problem that you then happen to be equipped to solve. Too romantic if you ask me.

Yes that's true. Most of the work has to go in the other direction, starting with the concept and then seeking to formalize it. I imagine a lot of the super-abstract stuff will actually not be crucial except maybe as an way of exploring the landscape.

>>8415866
>any problem in turbulence
I would like to mention that categories show some real promise for capturing key ideas in dynamical systems theory.

Reminder that Kochen_spekcker theorem is more and more trendy, or rather contextuality and that Bell theorem is less and less trendy, or rather locality.

>>8415866
>>Do you have a concise paper or whatever where it's pointed out where intuitionist logic jumps off constructive logic?
well whatever paper on geometric logic.


the typical texts are
-the maclane book, where he only discusses finitary geometric logic
-Makkai & Reyes, First order categorical logic model theoretical methods in the
theory of topoi and related categories
-all the work of vickers and his book Topology via logic, since geometric logic is the logical side of locale theory preserved under pullback functors (in fact, by definition of geometric functors, anything preserved by pullback functors is geometric)
-most things by coquand and vickers for topology
-coquand and henri lombardi, palgrem, spitters for algebra

the short papers are from vickers and the concrete work by coquand, like Constructive theory of Banach algebras

-Geometric logic in computer science, Theory and Formal Methods of
Computing
-Toposes pour les nuls
-Issues of logic, algebra and topology in ontology , Theory and Applications
of Ontology Computer Applications
-Continuity and geometric logic

Always have in mind that you can do locale theory, predicatively, intuitionistically, classically [the more classical you are, the more you rely on the frames]

>>8417630
>>8417630
also the most important papers; start with them

Locales and toposes as spaces, Handbook of Spatial Logics by vickers

and

Chapter 7
Invariants in Foundations: Geometric Logic by Marquis

>>8417641
>>Invariants in Foundations: Geometric Logic by Marquis


7.6 Using Geometric and Logical Invariants
As early as 1975, Andre Joyal suggested that the methods based on the notion of ´
the classifying topos are reminiscent of Hilbert’s ideas on the introduction and the
elimination of ideal elements in mathematical reasoning, usually known as Hilbert’s
program. The basic idea is to find a geometric or coherent formulation of a given
mathematical theory T, move to the category of concepts of T and the classifying
topos of the theory. Then, by the completeness results for geometric and coherent
theories, if there is a proof using classical logic and/or the axiom of choice, there
7.7 Summing Up 283
is a constructive proof of the same result. The construction of the classifying topos
amounts to the introduction of ideal elements that are then eliminated via the completeness results. Although my presentation makes it sounds as if it does not in fact
deliver a concrete constructive proof of the results, in practice, such proofs have
been found. (For a survey of such results in algebra, see for instance [50].)

>>8417642
As I have just said, the various theorems have to be “translated” adequately; that
is, an appropriate version of the theorem has to be found and then it is possible to
obtain a constructive proof of the new version. In many cases, these new versions
become the standard version when they are interpreted in the topos of sets, or, in the
case of topological spaces, when they are restricted to the correct class of topological
spaces. It should also be mentioned that the proofs depend on an interplay between
logical tools, geometrical tools and finally, categorical tools. They constitute perfect
illustrations of the multifaceted aspect of topos theory. Here is a sample of some of
the results that now have a constructive proof:
1. Tychonoff’s theorem asserts that a product of compact spaces is compact. The
standard proof depends on the axiom of choice. There are proofs that avoid the
use of the axiom of choice. (See, for instance, [118] and [123].)
2. Tychonoff’s theorem in turn implies the existence of the so-called Stone-Cech
compactification for certain spaces X, which, in a sense, is the maximal compactification of a space relative to a given embedding. Various constructive
proofs of this theorem can also be given. (See [10], [11], [13].)
3. The Stone-Weierstrass theorem can be proved constructively. (See [12].)
4. Gelfand duality can be given a contructive treatment. (See [14].)
5. The Hahn-Banach theorem in functional analysis is also known to depend on the
axiom of choice. Properly reformulated, a constructive version of the theorem
can also be given. (See [231].)
This is but a sample of an active field of research. Notice that in this case, topos theoretical methods are heuristic: they are used to find constructive proofs of results
that are known to depend on various parts of mathematics that are contentious from
a constructive point of view.

>>8411808
i mean, most people go in reverse. At least I did, you start with diff geom/de rham cohomology because it's physically intuitive with stokes theorem and shit. Then you move onto more general cohomology theories.

reminder that Barr theorem is classical

>>8417670
what do you do with cohomology in physics?

>>8419568
By de Rham's theorem, real cohomology is equivalent to integral de Rham cohomology, and from it you can derive cool stuff like Stoke's theorem (which I'm pretty sure you get when you apply Poincaré duality, but it may be more general). Chern-Weil theory tells you that cohomology corresponds to principle bundles, so you can also use cohomology to study symmetries. My immediate work involves characterizing properties of dynamical systems in terms of real cohomology and thereby in terms of de Rham cohomology, and applying the methods of Cech cohomology let you derive important invariants such as topological entropy. Long story short, cohomology is a central tool in many areas of physics (especially including field theories).