HOTT/UF ON SUNDAY, JULY 8TH

Days:

previous day

all days

View: session overviewtalk overviewside by side with other conferences

09:30-10:30 Session 36A

09:30 | Injective types and searchable types in univalent mathematics ABSTRACT. We characterize the injective types as the retracts of exponential powers of the universes. The injective (n+1)-types are the retracts of the universes of n-types, and in particular the injective sets are the retracts of powersets. We apply this to construct searchable types, with the property that every decidable subset has an infimum in a well founded, transitive, extensional order. This applies Yoneda-style machinery for types seen as infty-groupoids. |

11:00-12:30 Session 38H

11:00 | A Yoneda lemma-formulation of the univalence axiom |

11:30 | Robust Notions of Contextual Fibrancy ABSTRACT. We address two problems. First, in existing cubical models of HoTT, fibrancy of the dependent function type requires fibrancy of both domain and codomain. This is in contrast to what we see in category theory, where a functor space is already a category if the codomain is a category; the domain can be merely a quiver. Secondly, in a two-level type system that distinguishes between fibrant and potentially non-fibrant types, it is often not possible to provide an internal fibrant replacement operation as it does not commute with substitution. We identify a condition that is sufficient to address these problems, and observe that this condition is more easily met when considering notions of *contextual* fibrancy. |

12:00 | Cohesive Covering Theory |

14:00-15:30 Session 40H

14:00 | Cubical Computational Type Theory |

14:30 | The definitional symmetric cubical structure of types in type theory with equality defined by abstraction over an interval |

15:00 | Ordered Cubes |

16:00-18:00 Session 42G

16:00 | (Truncated) Simplicial Models of Type Theory |

16:30 | Towards the syntax and semantics of higher dimensional type theory |