nLab equivalence of (2,1)-categories

Redirected from "extensional type theories".
Contents

Context

Higher category theory

higher category theory

Basic concepts

Basic theorems

Applications

Models

Morphisms

Functors

Universal constructions

Extra properties and structure

1-categorical presentations

Equality and Equivalence

Homotopy theory

homotopy theory, (∞,1)-category theory, homotopy type theory

flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed

models: topological, simplicial, localic, …

see also algebraic topology

Introductions

Definitions

Paths and cylinders

Homotopy groups

Basic facts

Theorems

Contents

Idea

The concept of equivalence of (2,1)-categories is the concept of equivalence of (infinity,1)-categories restricted along the inclusion of (2,1)-categories into all (infinity,1)-categories.

Equivalently, the concept of equivalence of 2-categories restricted along the inclusion of (2,1)(2,1)-categories into 2-categories.

Properties

Hence in the presence of the axiom of choice, a (2,1)-functor f:𝒞𝒟f \colon \mathcal{C} \longrightarrow \mathcal{D} is an equivalence precisely if

  1. it is essentially surjective, hence surjective on equivalence classes of objects;

  2. it is fully faithful in that for all objects c 1,c 2𝒞c_1,c_2\in \mathcal{C} the 1-functor on hom-groupoids f c 1,c 2:𝒞(c 1,c 2)𝒟(f(c 1),f(c 2))f_{c_1,c_2}\colon \mathcal{C}(c_1,c_2) \longrightarrow \mathcal{D}(f(c_1),f(c_2)) is an equivalence of groupoids.

Created on April 16, 2015 at 07:17:57. See the history of this page for a list of all contributions to it.