HOTT/UF ON SUNDAY, JULY 31ST

Days:

next day

all days

View: session overviewtalk overviewside by side with other conferences

08:30-09:00Coffee & Refreshments

12:30-14:00Lunch Break

Lunches will be held in Taub hall and in The Grand Water Research Institute.

14:00-15:30 Session 14G

14:00 | Towards computing cohomology of dependent abelian groups |

14:30 | A Library of Monoidal Categories for Display and Univalence |

15:00 | The internal AB axioms |

16:00-17:30 Session 19E

16:00 | Internal languages of diagrams of ∞-toposes ABSTRACT. Homotopy type theory (HoTT) is a handy language for reasoning about an ∞-topos. However, sometimes we have more than one ∞-toposes related to each other by some functors, in which case plain HoTT is not sufficiently rich because the actions of the functors are not internalized. In this talk, we consider a certain class of diagrams of ∞-toposes for which plain HoTT remains a sufficiently rich internal language. We show that a special form of an inverse diagram of ∞-toposes is reconstructed internally to its oplax limit via lex modalities. Then plain HoTT as an internal language of the oplax limit can be used for reasoning about the original diagram. |

17:00 | An Experiment with 2LTT Features in Agda |