Homotopy Type Theory Discussed - Computerphile

Discussing Homotopy Type Theory with Professor Thorsten Altenkirch.

This video was filmed and edited by Sean Riley.

[KeithRozett]

2:35 "Some stupid programmer exploited that this was implemented in a certain way." Story of my life...

[Kram]

I guess it was kinda hard to do with Play-Doh but I wish you'd have done a demonstration of the different paths on a torus.
There are actually infinitely many different paths connecting any given point to itself.
The two most obvious ones are:
- Go along the big circle once.
- Go along the small circle (through the hole) once.
But actually you can also wind up paths. You won't be able to unwind them. So you can go through the hole twice or trice or n times... Each of those cannot be further simplified. That's what he was talking about.
Whereas on a sphere it really doesn't matter at all. No matter what you do, you *will* be able to shrink any given path to just a single point.

[combo]

The way this guy pronounces "theory" is so satisfying.

[emyru]

Thorsten?! I've been in his lectures before! Nice to see Homotopy Type Theory again. :)

[danieljensen]

Is Homotopy theory just topology with paths? Everything he talked about sounded like it was just a different approach to topology.

[TheDuckofDoom.]

This is even better than the main video.
Also there is some improvement with this latest Thorsten topic, maybe I am becoming accustomed to his accent, his english is improving, or the recording is higher quality.

[ylluminarious]

Me and my brain while listening to this:

Brain: what's that noise?
Me: what noise?
*whoosh*
Brain: there it is again!
Me: oh, i think i heard it. where's it coming from?
Brain: i think it's directly above us.
Me: *looks up*
Me: i don't see anything
*whoosh*
Brain: there it is again!
Me: whoa, what is that?
Brain: i guess it's called "Homotopy Type Theory"

[anywallsocket]

Objects are typically defined in such a way as to juxtapose their environment. Between the two opposite topologies I just mentioned are the Klein Objects.

The connection to Computer science can be understood in reference to a quote by David Wheeler: "All problems in computer science can be solved by another level of indirection." What he refers to is none other than the definition of further distinction between new objects and their environments - that is to say in discovering new Klein Objects.

[Gooberpatrol]

Bicycle tube. Because donuts don't exist in Europe.

[robchr]

How does this compare to Category Theory?

[bastiankraft]

If I wanted to learn this, what would the prequisites be?

[RussellJones]

How does the time taken to execute a module fit in with homotopy theory? Or does it only consider the values used by and produced by the modules? How about other characteristics of a module, such as memory requirements, thread count, etc. These could be relied upon by an external program, which would then operate differently if a replacement module was used.

[nster]

Could we get a video explaining the KRACK WPA2 vulnerability?

[bernardofitzpatrick]

Bicycle different structures but elements which are equal in similar ways - suddenly bell rang!

[soyoltoi]

What does he mean by implementation details in the context of mathematics? Axioms of models maybe?

[gzitterspiller]

I like this guy, he studies one of the hardest shits ever created and he kind.of tell you it is useless for a software engineer.

[KurtGodel]

What are the commercial applications of research into HTT?

[GuilhermeJohann]

It's only me that find very hard do understand Professor Thorsten Altenkirch accent? EN subtitles on his videos pls.

[Jacob]

Intriguing! Though the guy really doesn't make it easy to understand.

[michaelcharlesthearchangel]

The standard American Language inclusive of hyperPunctuation markers, upon standardization and legend-ing, should further the language-- the non-linear "linguistics", if you will, of t_pe theory and how We record (or recall rather), memorize assemblies of that manner of language\listing.
::
Intertranslation markers help One grapple with a non-linear language with principles, propositions\types, that may be applied in axioms to mathematics and geometry/chronometry.