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 bicategory is globally 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 bicategory for which the canonical function
is an equivalence of types for all objects , .
Created on August 20, 2024 at 14:43:39. See the history of this page for a list of all contributions to it.