FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
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
Location: Blavatnik LT1
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.

10:30-11:00Coffee Break
11:00-12:30 Session 38H
Location: Blavatnik LT1
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
12:30-14:00Lunch Break
14:00-15:30 Session 40H
Location: Blavatnik LT1
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
15:30-16:00Coffee Break
16:00-18:00 Session 42G
Location: Blavatnik LT1
16:00
(Truncated) Simplicial Models of Type Theory
16:30
Towards the syntax and semantics of higher dimensional type theory