Define 'D(f)'

[felixwellen]

$D(f)$ is the open subscheme given as the elements of an affine scheme $\mathrm{Spec}(A)$, where a function $f:\mathrm{Spec}(A)\to R$ has an invertible value.
$D(f)$ is a type which is an affine scheme and defines an (qc-)open proposition on $\mathrm{Spec}(A)$.

[felixwellen]

One problematic thing is to define the fp algebra $A_f$, which should probably be done in the cubical library. This might lead to a type checking speed problem.