Approaching the Yoneda Lemma
The Yoneda lemma is not the first thing to learn in category theory, but sooner or later it appears in studying the field. Unfortunately, there is quite a gap between the intuitive idea, "tell me your friends, and I will know who you are" , and its precise formulation. This talk aims to bridge this gap by introducing algebraic results in the middle, namely Cayley's theorem for groups and its generalization to semigroups. These are elementary enough, but at the same time they exhibit the conceptual step of representability, and the idea of studying all different things in a familiar form.
Outline/Structure of the Talk
- Abstract groups vs. permutation groups. Where to find a set to act on?
- Stating and proving Cayley's theorem.
- Generalizing to semigroups. The need for monoids: what happens without the identity?
- From semigroups to categories. Stating the Yoneda Lemma.
- Learn/refresh abstract algebraic concepts: groups, monoids, semigroups.
- See the high level of abstraction in category theory, in comparison with more concrete mathematical structures.
Developers who have heard of category theory, but find it intimidating beyond its basic concepts. Anyone enjoying mathematical abstraction.
Prerequisites for Attendees
There is no prerequisite for the talk, except willingness for following mathematical narrative.
schedule Submitted 7 months ago
People who liked this proposal, also liked:
Philip Wadler - (Programming Languages) in Agda = Programming (Languages in Agda)Philip WadlerProfessor of Theoretical Computer ScienceUniversity of Edinburgh
schedule 8 months agoSold Out!
The most profound connection between logic and computation is a pun. The doctrine of Propositions as Types asserts that propositions correspond to types, proofs to programs, and simplification of proofs to evaluation of programs. The proof of a conjunction is a pair, the proof of a disjunction is a case expression, and the proof of an implication is a lambda expression. Proof by induction is just programming by recursion.
Dependently-typed programming languages, such as Agda, exploit this pun. To prove properties of programming languages in Agda, all we need do is program a description of those languages Agda. Finding an abstruse mathematical proof becomes as simple and as fun as hacking a program. This talk introduces *Programming Language Foundations in Agda*, a new textbook that is also an executable Agda script---and also explains the role Agda is playing in IOHK's new cryptocurrency.
Bartosz Milewski - A Taste of Type TheoryBartosz MilewskiMath EvangelistProgramming Cafe
schedule 8 months agoSold Out!
We use types in programming, often without realizing how deeply rooted they are in the foundations of mathematics. There is a constant flow of ideas from type theory to programming (and back). We are familiar with algebraic data types; inductive types, like lists or trees; we've heard of dependent types and, in the future, we might encounter identity types and possibly get familiar with elements of homotopy type theory. I can't possibly talk about all of this, but I'll try to give you a little taste.
Andy Kitchen - Meta-quinesAndy KitchenCommittee MemberMelbourne Functional Programming Association
schedule 7 months agoSold Out!
A quine is a program that outputs its own source code, but can you create a 2 quine, a pair of programs that output each other with an A->B->A->B cycle? What about between different languages? Can you gzip your own source code? Is there a structured way to do this with theory? All these questions will be somewhat answered, in ways that will make your head hurt... math-a-magical demos and over 9000 layers of meta-ness await!
Ken Scambler - Applied Category Theory - The Emerging Science of CompositionalityKen ScamblerSoftware ArchitectMYOB
schedule 9 months agoSold Out!
What do programming, quantum physics, chemistry, neuroscience, systems biology, natural language parsing, causality, network theory, game theory, dynamical systems and database theory have in common?
As functional programmers, we know how useful category theory can be for our work - or perhaps how abstruse and distant it can seem. What is less well known is that applying category theory to the real world is an exciting field of study that has really taken off in just the last few years. It turns out that we share something big with other fields and industries - we want to make big things out of little things without everything going to hell! The key is compositionality, the central idea of category theory.
This talk will introduce the emerging field of applied category theory, with the aims of:
- Giving attendees a broad overview of cutting-edge applications of category theory
- Building an understanding of a small number of the most important core concepts
- Getting attendees excited, inspired to learn more, and equipped to apply some basic concepts to their work