[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] ## Subset collection in dependent type theory In dependent type theory, an entire relation on a type $A$ is a family of [[h-propositions]] $$x:A, y:A \vdash R(x, y)$$ $$x:A, y:A \vdash p(x, y):\mathrm{isProp}(R(x, y))$$ such that $$x:A \vdash q(x):\exists y:A.R(x, y)$$ category: redirected to nlab