nLab locally univalent bicategory

Locally univalent bicategories


2-Category theory

Higher category theory

higher category theory

Basic concepts

Basic theorems





Universal constructions

Extra properties and structure

1-categorical presentations

Locally univalent bicategories


In an intensional type theory such as homotopy type theory, a bicategory is locally univalent if every hom-category is a univalent category.

More specifically, it is a bicategory CC for which the canonical functions

idtoiso 2,1(f,g):(f=g)inv2cell(f,g)idtoiso^{2,1}(f, g):(f = g) \to inv2cell(f, g)

is an equivalence of types for all objects a:Ob(C)a:Ob(C), b:Ob(C)b:Ob(C), and morphisms f:Mor C(a,b)f:Mor_C(a,b) and g:Mor C(a,b)g:Mor_C(a,b).

In set-level foundations

A locally univalent bicategory in set-level foundations is the same thing as a locally gaunt bicategory whose type of objects is a set.

See also


Last revised on September 2, 2022 at 10:51:47. See the history of this page for a list of all contributions to it.