[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Function types a la Russell and a la Tarski In the same way that universes could be expressed as category: redirected to nlab