Tags:contextual fibrancy, fibrancy of the function type, fibrant replacement and right lifting property
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.