This is pretty deep stuff, it took me a long time to understand the background ideas, such as the Curry-Howard isomorphism and homotopy theory. From the Curry-Howard correspondence, type theory corresponds to propositional logic. But we also need predicate logic to describe more complex stuff. So, to handle predicates we need types to have subtypes, similar to sets having subsets. Such structures (ie, the predicates) are "fibrations" over the base set, borrow the idea from algebraic topology. Now, it has long been known that propositional logic is more or less "isomorphic" to topology (ie, the structure of open sets). So the fibration of predicate logic above is over the base topology of propositional logic. Thus the idea of homotopy theory enters because it characterizes some properties about the predicates and the underlying propositions.
One important piece is missing - what is the structure of a space induced by a type? It is not immediately clear that such a space could have reasonable topology and paths at all. Maybe all we can do is pointwise topology? Or we can imagine infinite number of topologies - thus a path in one might not be a path in another. The there is a jump from “type is a space, points are elements of a type” to “paths between types”. For such a path between types we need a space where points are types themselves which was never introduced. With these basic things lacking content of the whole lecture seems opaque to me.
You never really descend on the "topology" level. Note the contrast between "topology" and "homotopy": the latter does not deal with points and topological structures (sets of opens). Now, if one wants to go to homotopy theory from HoTT and interpret types as [homotopy classes of] spaces, then there are different models, such as Kan simplicial sets, which the Univalence Exion owes its existence to. A path between types takes place in the "universe type" U.
@@homology I don't think I fully understood your comment, too mathy for my :) I guess if you have a path then you must have a structure on a set that would allow it. The simplest structure of this sort I can think of is topology. In other words how do you move along the path?
@@andreyverbin Homotopy in HoTT is synthetic, meaning that it is not constructed inside some ambient theory (e.g. via sets with structures), but rather is "already there". Compare with synthetic geometry (working in a thing with Euclidean axioms) vs analytic geometry (working in a set of tuples of numbers which one thinks of as coordinates). In particular, paths in HoTT are a primitive, built-in notion. By definition they are just elements of identity types (so one writes p: a = b). Then "transport along a path" is a function whose existence follows formally from the definition of an identity type (which in turn is defined by its induction principle, much in the way the natural numbers are defined as the type enabling induction).
I felt like I'm back to university and hate math again. Does it mean I have to fast forward 3 years and I will fall in love with those ideas because I find a reasonable explanation to them written by original authors and not this in a world nonsense rubbish. I don't know ... yet!
In this context a CPO would be a "complete partial order". It is a mathematical structure, which is useful for defining semantics for programming languages, among other things.
He might mean en.wikipedia.org/wiki/Complete_partial_order. At 7:45 he mentioned "denotational semantics" and the wiki article mentions it too. The problem is the wiki article defines CPO as "a Set with some properties" and Dan Licata makes a distinction between Sets and CPOs. So we're screwed. Except that I found cs.uwaterloo.ca/~david/cs442/lect-SEMANTICS.pdf which at the first glance looks like a matrix screensaver to me.
CPOs are "complete partial orders". They are structures used by Dana Scott to construct some models in denotational semantics. CPOs are sort of like programs that return *partial* results. Each time you iterate a program, it gives a result closer to the final answer. Like a progressive approximation that gets closer and closer to some fixed point. The functions that map CPOs to CPOs may have the "continuous" property that come from topology. By using this notion, Dana Scott is able to construct a *domain* where the set of functions from A --> A is isomorphic to the set A itself. It is impossible in classical set theory for a set A to be equal to its power set. But Dana Scott succeeded in establishing such an isomorphism, which is surprising. This is one of the cornerstone theorems in "domain theory".
It's not necessarily that his voice is high-pitched, is that his speech pattern has an "effeminate", valley girl-ish tone. If he spoke in a more masculine tone, he'd have a far deeper voice.
![[Intro to HoTT - OLD] Martin-Löf Type Theory: Speaking the Language](http://i.ytimg.com/vi/TeY5niDR8yE/mqdefault.jpg)
This is pretty deep stuff, it took me a long time to understand the background ideas, such as the Curry-Howard isomorphism and homotopy theory.
From the Curry-Howard correspondence, type theory corresponds to propositional logic. But we also need predicate logic to describe more complex stuff. So, to handle predicates we need types to have subtypes, similar to sets having subsets. Such structures (ie, the predicates) are "fibrations" over the base set, borrow the idea from algebraic topology.
Now, it has long been known that propositional logic is more or less "isomorphic" to topology (ie, the structure of open sets). So the fibration of predicate logic above is over the base topology of propositional logic. Thus the idea of homotopy theory enters because it characterizes some properties about the predicates and the underlying propositions.
Provides nice intuition about how ideas from homotopy type theory will appear in functional programming.
Absolutely cool if you can talk that freely and clear at the same time.
It is a great talk. Finally I understand what is homotopy type theory for Computer Programming.
One important piece is missing - what is the structure of a space induced by a type? It is not immediately clear that such a space could have reasonable topology and paths at all. Maybe all we can do is pointwise topology? Or we can imagine infinite number of topologies - thus a path in one might not be a path in another.
The there is a jump from “type is a space, points are elements of a type” to “paths between types”. For such a path between types we need a space where points are types themselves which was never introduced.
With these basic things lacking content of the whole lecture seems opaque to me.
You never really descend on the "topology" level. Note the contrast between "topology" and "homotopy": the latter does not deal with points and topological structures (sets of opens). Now, if one wants to go to homotopy theory from HoTT and interpret types as [homotopy classes of] spaces, then there are different models, such as Kan simplicial sets, which the Univalence Exion owes its existence to.
A path between types takes place in the "universe type" U.
@@homology I don't think I fully understood your comment, too mathy for my :) I guess if you have a path then you must have a structure on a set that would allow it. The simplest structure of this sort I can think of is topology.
In other words how do you move along the path?
@@andreyverbin
Homotopy in HoTT is synthetic, meaning that it is not constructed inside some ambient theory (e.g. via sets with structures), but rather is "already there". Compare with synthetic geometry (working in a thing with Euclidean axioms) vs analytic geometry (working in a set of tuples of numbers which one thinks of as coordinates).
In particular, paths in HoTT are a primitive, built-in notion. By definition they are just elements of identity types (so one writes p: a = b). Then "transport along a path" is a function whose existence follows formally from the definition of an identity type (which in turn is defined by its induction principle, much in the way the natural numbers are defined as the type enabling induction).
I felt like I'm back to university and hate math again. Does it mean I have to fast forward 3 years and I will fall in love with those ideas because I find a reasonable explanation to them written by original authors and not this in a world nonsense rubbish. I don't know ... yet!
Good talk. Awesome possibilities.
What is the best programming language for HoTT?
anyone know what CPOs are?
In this context a CPO would be a "complete partial order". It is a mathematical structure, which is useful for defining semantics for programming languages, among other things.
He might mean en.wikipedia.org/wiki/Complete_partial_order. At 7:45 he mentioned "denotational semantics" and the wiki article mentions it too. The problem is the wiki article defines CPO as "a Set with some properties" and Dan Licata makes a distinction between Sets and CPOs. So we're screwed. Except that I found cs.uwaterloo.ca/~david/cs442/lect-SEMANTICS.pdf which at the first glance looks like a matrix screensaver to me.
CPOs are "complete partial orders". They are structures used by Dana Scott to construct some models in denotational semantics. CPOs are sort of like programs that return *partial* results. Each time you iterate a program, it gives a result closer to the final answer. Like a progressive approximation that gets closer and closer to some fixed point.
The functions that map CPOs to CPOs may have the "continuous" property that come from topology. By using this notion, Dana Scott is able to construct a *domain* where the set of functions from A --> A is isomorphic to the set A itself. It is impossible in classical set theory for a set A to be equal to its power set. But Dana Scott succeeded in establishing such an isomorphism, which is surprising. This is one of the cornerstone theorems in "domain theory".
"If you know some category theory, then everywhere I said 'path', then "???? (16:36)
Thanks! Good!
@@marshacd "replace it with morphism and a groupoid"
good luck, audience
Great content!
Whether we are in a world or not is itself in the world of set theory ironically enough. lol
Its now obvious that hott has very little practical programming value.
I don't think that's totally true, or a very productive thought.
It's not necessarily that his voice is high-pitched, is that his speech pattern has an "effeminate", valley girl-ish tone. If he spoke in a more masculine tone, he'd have a far deeper voice.
"Okay?"