Post #2385819
2026-05-01 14:19 UTC
@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.
Replies (1)
-
@ncf@types.pl 2026-05-01 14:23
@trebor@types.pl Nice, thanks! I indeed don't really need the categorical structure on A here (it doesn't even need to be a universe).