Homotopy Type Theory precategory > history (Rev #9, changes)

Showing changes from revision #8 to #9: Added | Removed | Changed

Contents

Whenever editing is allowed on the nLab again, this article should be ported over there.

Definition

In set theory

A precategory AA consists of the following.

  • A preset A 0A_0, whose elements are called objects. Typically AA is coerced to A 0A_0 in order to write xAx \in A for xA 0x \in A_0.

  • For each a,bAa,b \in A, a set hom A(a,b)hom_A(a,b), whose elements are called arrows or morphisms.

  • For each aAa \in A, a morphism 1 ahom A(a,a)1_a \in hom_A(a,a), called the identity morphism.

  • For each a,b,cAa,b,c \in 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,bAa,b \in A and fhom A(a,b)f \in hom_A(a,b), we have f=1 bff=1_b \circ f and f=f1 af=f\circ 1_a.

  • For each a,b,c,dAa,b,c,d \in A,

    fhom A(a,b),ghom A(b,c),hhom A(c,d)f \in hom_A(a,b),\ g \in hom_A(b,c),\ h \in hom_A(c,d)

    we have h(gf)=(hg)fh\circ (g\circ f)=(h\circ g)\circ f.

In homotopy type theory

A precategory AA consists of the following.

  • A type A 0A_0, whose elements are called objects. Typically AA is coerced to A 0A_0 in order to write x:Ax:A for x:A 0x:A_0.

  • For each a,b:Aa,b:A, a set 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 f=1 bff=1_b \circ f and f=f1 af=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 h(gf)=(hg)fh\circ (g\circ f)=(h\circ g)\circ f.

Properties

In homotopy type thoery, there are two notions of “sameness” for objects of a precategory. On one hand we have an isomorphism between objects aa and bb on the other hand we have equality of objects aa and bb. In set theory, if the preset AA is an \infty-groupoid, there a notion of path space of objects aa and bb which corresponds to equality of objects in homotopy type thoery. However, for general presets there is only one notion of “sameness” for objects in a precategory.

There is a special kind of precategory called a category where these two notions of equality coincide and some very nice properties arise.

Lemma 9.1.4 (idtoiso)

if AA is a precategory and a,b:Aa,b:A, then there is a map

idtoiso:(a=b)(ab)idtoiso : (a=b) \to (a \cong b)

Proof. By induction on identity, we may assume aa and bb are the same. But then we have 1 a:hom A(a,a)1_a:hom_A(a,a), which is clearly an isomorphism. \square

Examples

See also

References

category: category theory

Revision on June 7, 2022 at 20:56:29 by Anonymous?. See the history of this page for a list of all contributions to it.