nLab H-category


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



Paths and cylinders

Homotopy groups

Basic facts


Higher algebra



The oidification of an A3-space/H-monoid?, or equivalently, a category internal to Ho(Top) *Ho(Top)_*.



A H-category or A3-spaceoid is a category internal to the classical homotopy category of topological spaces Ho(Top), or in the homotopy category Ho(Top) *Ho(Top)_* of pointed topological spaces.

Internally in an (infinity,1)-category

For the time being see category object in an (infinity,1)-category#HCategoryTypes.

In homotopy type theory

In homotopy type theory, a H-category or A3-spaceoid is a type AA with

  • For each a,b:Aa,b:A, a type hom A(a,b)hom_A(a,b), whose elements are called arrows or morphisms.

  • For each a:Aa:A, a morphism 1 a:hom A(a,a)1_a:hom_A(a,a), called the identity morphism.

  • For each a,b,c:Aa,b,c:A, a function

    hom A(b,c)hom A(a,b)hom A(a,c)hom_A(b,c) \to hom_A(a,b) \to hom_A(a,c)

    called composition, and denoted infix by gfgfg \mapsto f \mapsto g \circ f, or sometimes gfgf.

  • For each a,b:Aa,b:A and f:hom A(a,b)f:hom_A(a,b), we have the left unitor λ f:f=1 bf\lambda_f:f=1_b \circ f and the right unitor ρ f:f=f1 a\rho_f:f=f\circ 1_a.

  • For each a,b,c,d:Aa,b,c,d:A,

    f:hom A(a,b),g:hom A(b,c),h:hom A(c,d)f:hom_A(a,b),\ g:hom_A(b,c),\ h:hom_A(c,d)

    we have the associator α f,g,h:h(gf)=(hg)f\alpha_{f, g, h}:h\circ (g\circ f)=(h\circ g)\circ f.

See also

Last revised on August 30, 2022 at 18:22:26. See the history of this page for a list of all contributions to it.