Egbert Rijke: Homotopy limits in type theory
Source: Mathematics and theoretical computing seminar
Danes se bo seminar za osnove izjemoma dobil kar v času kosila v skupni sobi. S seboj prinesite sendvič in ob prebavljanju poslušajte Egbert Rijkeja, ki bo govoril o homotopski teoriji tipov.
Abstract: One may wonder how much of the category theoretical notions can be transported to the setting of homotopy type theory. Such a question is part of the task whether the class of homotopy sets forms a predicative topos, meaning that homotopy sets have as much good properties as one could wish. With limits of diagrams this can be done quite easily, but already here we see a slightly surprising consequence: the monomorphisms in homotopy type theory may not be those functions just satisfying cancellation from the left.