Re: [HoTT] Re: Precategories, Categories and Univalent categories

[Andrew Polonsky <andrew.polonsky@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 1530 bytes --]

The intuitive notion of a category is given by the dependently-sorted 
algebraic theory of categories.

In the ZFC metatheory, a standard model of this theory yields the usual 
mathematical concept of a category.

In the MLTT metatheory, a standard model of this theory yields the concept 
of a precategory.

The subtle issue is how to treat the equality predicate, appearing in the 
identity and associativity axioms.

In set theory, equality is a former of atomic formulae, which are a 
different syntactic category than sets (which interpret the types/domains 
of the given language).

In type theory, equality is interpreted as any other type, in accordance 
with "the formulae-as-types notion of construction".

However, more modern type theories, like HoTT or CubicalTT, have a 
different, "native" conception of equality, so the "natural" notion of 
category in these theories will accordingly be different as well.

One day, there might be a metatheory which is generally accepted as 
providing a superior "natural" notion of a category, that avoids the 
awkward points of the set-theoretic one.

Until then, it is best to be precise with language, always being explicit 
which specific concept is meant.

Cheers,
Andrew

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.2: Type: text/html, Size: 1990 bytes --]