Post #2385820

@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).