You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Tim Hosgood (Aug 23 2021 at 15:37):Thursday the 26th of August, 17:00 UTC
Abstract:
Intensional Type Theory and Category Theory ought to fit well together, but the current practical experience of representing concepts from one with the tools of the other is often quite strained. On the one hand, fibrational approaches to dependency often seem heavy. On the other hand, definitional equality in type systems often falls way short of delivering even the simplest of coherences. In this talk, I shall reflect on the problems and search for opportunities. What has to change to make type theoretic proof assistants a good medium for categorical approaches to programming and proof? I wish I knew the answer to that question! I can at least offer a few clues. For example, I shall exhibit a universe of indexed inductively defined datatypes which exhibit nontrivial presheaf structure by construction.
YouTube: https://youtu.be/05IJ3YL8p0s
Zoom: https://topos-institute.zoom.us/j/5344862882?pwd=Znh3UlUrek41T3RLQXJVRVNkM3Ewdz09
Tim Hosgood (Aug 26 2021 at 16:31):@Conor McBride will be giving this talk in half an hour!
Henry Story (Aug 27 2021 at 04:54):I wonder if Cubical Agda is an instance of what @Conor McBride was describing.
(From what I understand there is some extra category theoretic machinery added to Agda for cubical to help make structure easier to work with.)
Conor McBride (Aug 27 2021 at 09:10):It's certainly a much better place to negotiate "the equality type you really mean" than anything with inductive equality. And there are certainly attempts in that community to enhance the equational theory the machine decides: you can add rewriting rules (a bit dangerously). Good steps in the right direction, but still a long way to go.
Henry Story (Aug 28 2021 at 06:40):In the setup I am working in the whole web is my environment. Terms are URLs and their meaning is found by fetching that URL: an RDF Graph). I mention that because as I remember @Conor McBride's talk was about extending the power of the environment, and that is one way to go.
Henry Story (Aug 28 2021 at 06:51):or in short: Can web-cats and types be best friends?
:smiley_cat:
dan pittman (Aug 11 2022 at 23:43):I just watched this, but I don't have enough context to keep up. Around 13:30, he draws as , and then says, "I'm going to write this as ", but I don't understand what's happening with the . I don't get what's indexing what there.