I've read the beginning and the jumped the history part to the end of the second chapter (see >>7855038) but haven't looked at the end, where he discusses his proposal for the position of logic within the foundations.
If you follow all the business around Voevodsky and friends, their in part public fights about the emphasis of different topics of their collaboration is quite fun. He is essentially mad they wrote that typey book and went on doing more of his own stuff, and writing his own article https://en.wikipedia.org/wiki/Univalent_foundations and it reads like it.
>>7857168 ad: Mhm... looking at the history parts I skipped, they seem to give a good overview of the development of logic (and set and cats) since 1890.
>>7857187 There is a one week workshop about it at this very moment in Bonn. If you read the abstract of Voevodsky morning series (pic related), you see his current attempts is to find a good model of it (univalence I guess) in ZFC. Indeed, it would be very cool if set theories jumped on that wagon and investigate some features of that world within their own playground.
I'd like to have a dependently typed language with simple semantics ready to do some programming right now. I'm thinking about outlining the syntax of such a language, actually, because I want to implement some physics in it (differential geometry).
If I understand the univalence axiom
[math] ua: (A=B) \to (A \cong B)[/math]
correctly, then it's indeed an important thing for math. Personally I find the type theory (Martin-Löf) equality extremely tiresome, all the formal substitution rules that you just igonore or just do if you do normal math. Or path induction proofs - I don't know if this stuff can become second nature to any "normal person". The biggest problem with HoTT et al. that I see is that people "like me" don't care about proofs of known mathematical "truths". Certified programming is cool, and automatic term generation is awesome, but the language must be effective to use.
>>7857194 >There is a one week workshop about it at this very moment in Bonn. Nice, I didn't know that. There's also one in May at the Fields Insitute and one in Porto in June. >you see his current attempts is to find a good model of it (univalence I guess) in ZFC. I first read about this on /sci/ a few weeks back. IIRC, the intent is to create a model of HoTT in ZFC so that the wider mathematical community is more amenable to use and contribute to the programme. >I'd like to have a dependently typed language with simple semantics ready to do some programming right now. I've been following some type theory/PL people on Twitter and various mailing lists and there seems to be a lot happening in this area at the moment it seems. We have full-fledged languages like Coq, Agda and Idris, and there are also smaller, two/three-person projects building on MLTT, but also observational and computational theories. I don't have the links on me right now, but I can hit you up later if you're interested.
>>7857168 >>7857194 I think we're opposites on this. I'm a math student but I'm far more interested in the type theory and proof theory side of things than I am with the math itself. I'm currently in a HoTT course as well and though I'm interested in the foundational aspect of the topic I've found I'm totally not interested in homotopy theory.
I'm pretty sure I'm going to switch over to computer science since their type theory/mathematical logic/proof theory stuff becomes more and more relentlessly formal and rigorous the further up you go while the opposite is true on the math side of things.
>>7857210 I'm not interested in homotopy theory porpper either (as in, what is the so and so group of S^7), but categories and sheaves are more native in that language and cool people speak about interesting subjects in terms of those.
The philosophical side is relevant to me too. E.g. I always like to point out that you if you use the standard model for the pair and natural numbers in a set theory like ZFC, namely
I use Haskell rudimentary and if there comes along a statically typed language with [math]\Pi[/math] and [math]\Sigma[/math], I'd totally start taking informal notes in those terms too more, because then the step to make something computationally out of it would be so small. Cooler, as I said, if someone would write a super strong compiler that generates terms of such a type for you. That's where we should go. Haskell already does this sometimes, when some type has a unique term (e.g. some functor actions on arrows in C are fully determined just by specifying you want to consider a functor from C to D that maps objects in this and that way. The arrow maps are then sometimes unique and haskell ghc is clever enough to infer the code for you)
If that's not enough for you, if you were to enumerate theorems of your language, you'd produce such mathematically meaningless shizzle. This can't happen in typed or categorical foundations - that's why the latter are better. Set theory should just be a theory expressible in your world imho, not be at the core. Not material set theory at least.
Which is a very weird dubious construction in my opinion. No less weird than saying something like
I don't particularly mind the issue you pointed out since it comes up in many other theories as well. For instance in lambda calculus your "numbers" are just special terms (read: functions) dubbed "church numerals" and you end up with all sorts of computations being "equal" to a number.
>The standard Hilbert-style formal axiomatic method serves us as a tool for studying a logical structure of mathematical theories but not as a tool for presentation and logical justification of these theories (as Hilbert and his followers wanted). The requirement according to which a given theory T must be formalizable in principle constitutes a very weak necessary (but not sufficient) condition for saying that T well-standing. Notice that a contradictory theory can be well formalizable.
>>7857282 Me again. I had only skimmed the article and had missed the point. The derive functionality has been around since as long as I've been using Haskell so I didn't even realize it was trying to show it off as a new feature.
>>7857276 I don't mean any offense but perhaps this was not the article you meant to link (or I am missing the point completely)?
>>7857278 >For instance in lambda calculus your "numbers" are just special terms (read: functions) dubbed "church numerals" and you end up with all sorts of computations being "equal" to a number. There are many ways to represent numbers (natural, integers, rational, algebraic reals and complex) in lambda calculi. For instance, in Calculus of Inductive Constructions, you would define an inductive data type like
so, from i gather from here http://philomatica.org/wp-content/uploads/2015/04/rodin.pdf
this is his claim >In Mathematics the constructive approach is already proved effective: the proof of 4-colors theorem is formalized through Coq (based on MLTT, which is the logical base of HoTT). Given the prominence of model-building in Physics there is a reasonable hope that this method will also work more successfully in Physics.
>IF HoTT proves to be a full-fledged foundation of mathematics it will also serve as a mathematical foundation for the mathematized Physics. Then it will covert physical theories into constructive axiomatic theories automatically. Unlike Set Theory the Homotopy (Type) Theory has some natural physical interpretations. That makes HoTT a strong candidate to the role of basic “constructor” out of which one may build physical (interpreted) theories. Theories built with HoTT are computable ) unless one adds to MLTT new axioms such as Univalence, which may be indeed strongly motivated by logical, geometric and perhaps also specific physical reasons. so apparently, it is just another attempt to formalize discourses, up to physics
>>7857296 pic related, could have googled that yourself
>>7857278 >and you end up with all sorts of computations being "equal" to a number. Yes, but what your primary notion of equality is really is and what it's not can be internalized (Martin Löf-type theory) and forced to be equal to the structual notion you deem relevant (univalence)! That's exactly what the fuzz is about
being required to be an equivalence (an ≅ one level up). Like in category theory where things defined by a universal property are equivalent. So ≅, and in turn =, is, for every structure, only what you make it it to.
>>7857290 Given Curry Howard, to my ears, that's like asking if you I have faith in predicate logic.
If you ask some guy to write >a function that maps a number to a list of it's prime factors, e.g.
70 to (2,5,7)
then in C or Java you can start a scrip specifying in one line that the input is an integer, "int" in Haskell you can demand that the code is a function mapping an integer to some list of integers "Int -> [Int]" in Idris you can can already specify that the list can't possibly be longer than the number itself (70 can't have over 70 prime factors) and in a neat future dependently typed language language you can specify that he writes >a function that maps a number to a list of it's prime factors and the compiler (type checker) will say fuck you if his code doesn't do what it should be. If your type theory is as strong as (higher) order logic, coding is just about coming up with one of the extensionally equivalent terms of that type that captures all non-meta (e.g. runtime) specifications (you come up with a proof)
>>7857282 It's more ad hoc and doable with less brain effort, I guess. (I take your claim that three gives rise to a Comonad as a given, not that you make fun of me by putting up a trap here) >>7857305 The article is also 6 years old now, but the derive tool is what I meant.
>>7857308 He was getting ideas out of Hegels science of logic last year (because Laywere did it some decades ago) and I was reading along on the nforum. My understanding of the point in pic related.
Urs did his PhD thesis on classical field theory in stacks (using the tools of algebgraic topology, i.e. sheaves on topological spaces, but not using sets but groupoids) and there the groupoids have things like gauge transformations between fields (e.g. electrical fields) natively build into them. As the HoTT bandwagon is going on and everything becomes a synthetic theory within a type theory, he's looking at the axiomatization of those (higher) stacks in terms of adding some functors to HoTT.
For the first level: The comonad-monad graph FGa -> a -> GFa is also what you find if 'a' is a space and FGa, GFa are the two trivial topologies (the thing itself is the only open set vs. every element of the set is open (discrete topology)).
This is sets -> topology, differential structure comes later, bosons and fermionic structure even later. And apparently he can force the axioms for those in terms of (co-)monads too.
>>7857210 >I think we're opposites on this. Yes I guess the above is not exactly the theorem proving side of HoTT ^^
>>7857329 >and the compiler (type checker) will say fuck you if his code doesn't do what it should be. If your type theory is as strong as (higher) order logic, coding is just about coming up with one of the extensionally equivalent terms of that type that captures all non-meta (e.g. runtime) specifications (you come up with a proof) This too
Thread replies: 31 Thread images: 9
Thread DB ID: 513542
All trademarks and copyrights on this page are owned by their respective parties. Images uploaded are the responsibility of the Poster. Comments are owned by the Poster.
This is a 4chan archive - all of the shown content originated from that site. This means that 4Archive shows their content, archived. If you need information for a Poster - contact them.
If a post contains personal/copyrighted/illegal content, then use the post's [Report] link! If a post is not removed within 24h contact me at email@example.com with the post's information.