Post #2061465
2026-05-01 13:10 UTC
Is there a name in category theory for the following situation? Two categories A and U with functors i : A → U and r : U → A such that for all X : U, irX retracts onto X (maybe naturally in X?). Like a "retraction up to retraction" or something.
I ask because the type theoretic version of that where A : U are nested universes is enough to set up Russell's paradox (well known).
Replies (1)
-
@trebor@types.pl 2026-05-01 14:19
@ncf@types.pl There is the notion of a dominant functor, which is a functor i : A -> U such that for every object Y : U, there exists an object X : A such that we have a retract Y -> iX -> Y. There is no functoriality requirement on the r map though, and in fact A can be a discrete category.