Definitions
Transfors between 2-categories
Morphisms in 2-categories
Structures in 2-categories
Limits in 2-categories
Structures on 2-categories
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
In an intensional type theory such as homotopy type theory, a locally univalent bicategory is univalent if a Rezk completion condition is satisfied for the objects of the bicategory: equality of objects is adjoint equivalence of objects.
More specifically, it is a locally univalent bicategory for which the canonical function
is an equivalence of types for all objects , .
A univalent bicategory in set-level foundations is the same thing as a locally posetal gaunt category.
Last revised on February 15, 2023 at 08:15:04. See the history of this page for a list of all contributions to it.