# nLab locally univalent bicategory

Locally univalent bicategories

### Context

#### 2-Category theory

2-category theory

Definitions

Transfors between 2-categories

Morphisms in 2-categories

Structures in 2-categories

Limits in 2-categories

Structures on 2-categories

#### Higher category theory

higher category theory

# Locally univalent bicategories

## Definition

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 $C$ for which the canonical functions

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

is an equivalence of types for all objects $a:Ob(C)$, $b:Ob(C)$, and morphisms $f:Mor_C(a,b)$ and $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.