Homotopy Type Theory quiver > history (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

Contents

Definition

A quiver 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 type hom A(a,b)hom_A(a,b), whose elements are called arrows or morphisms.

See also

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