In the paper about Cubical Agda you may find that partial elements Partial r A “are equal whenever they reduce to equal terms for all the possible assignment of variables that make r equal to i1”.
Firstly you should ensure that these partials are correctly defined, i.e. for all $i$ and $j$ we have $\Gamma, \phi_i ∧ \phi_j ⊢ u_i \equiv u_j$ (see CCHM, page 9, figure 3), but this should be performed earlier, while deducing type of $[\phi_i \mapsto u_i]$.
Then yes, you need to check that two partials are defined on equal r’s, i.e. $\bigvee_i \phi_i = \bigvee_j \psi_j$ (otherwise they have different types).
What to do next depends on the way you store partials.
Assume that any $\phi_i$ is a face in the form $(\phi_i^1 = d_{\phi_i}^1)\ (\phi_i^2 = d_{\phi_i}^2)\ ...\ (\phi_i^k = d_{\phi_i}^k)$ (where $\forall m: d^m_{\phi_i} \in \{0,\ 1\}$), then $\bigvee_i\phi_i$ is equal to $1$ iff for some $i$ we have $\phi_i^m \equiv d^m_{\phi_i}$ for all $m$ (since $\bigvee_i\phi_i$ is a disjunction and each $\phi_i$ is a conjunction). We know at this point that $\bigvee_i \phi_i = \bigvee_j \psi_j$, so for some $j$ we have $\forall m: \psi_j^m \equiv d^m_{\phi_j}$. Then $[\phi_i \mapsto u_i]$ reduces to $u_i$ and $[\psi_j \mapsto v_j]$ to $v_j$. If we assume that each $u_i$ and $v_j$ does not contain any $\phi_i^m$ and $\psi_j^m$ respectively (otherwise you should replace in $u_i$ each $\phi_i^m$ with $d^m_{\phi_i}$ and each $\psi_j^m$ in $v_j$ with $d^m_{\psi_j}$ and probably perform some computations), then it remains perform conversion-check between $u_i$ and $v_j$. And this is what, for example, cubicaltt does. My checker also performs the same thing (Map.equal in OCaml checks for key equality too).
Of course, as Trebor said, we can check $\Gamma, \phi_i ∧ \psi_j ⊢ u_i \equiv v_j$ for all $i$ and $j$, but if partials are correctly defined and for each pair $\phi_i \equiv \psi_j$ we have $u_i \equiv v_j$, then assuming some $i$ and $k$ we have for some $j$ such equality: $\Gamma, \phi_i \equiv \psi_j ⊢ u_i \equiv v_j$. Since partials are defined correctly, we have $\Gamma, \psi_j ∧ \psi_k ⊢ v_j \equiv v_k$. Combining these, we obtain $\Gamma, \phi_i ∧ \psi_k \equiv \psi_j ∧ \psi_k ⊢ u_i \equiv v_j \equiv v_k $ and $ \Gamma, \phi_i ∧ \psi_k ⊢ u_i \equiv v_k $ for all $i$ and $k$. So it’s enough to conversion-check only $u_i$ and $v_j$ with equal $\phi_i$ and $\psi_j$.
But this is not the only one way to store partials. For example, if you don’t have diagonals (faces like $(i = j)$ for free $i$ and $j$), you may assume that each $\phi_i$ is an arbitrary element of $\mathrm{I}$, so $[i ∧ -j \mapsto u, k \mapsto v]$ corresponds to $[(i = 1) \mapsto u, (j = 0) \mapsto u, (k = 1) \mapsto v]$. Then on the second step you may convert $\bigvee_i \phi_i \equiv \bigvee_j \psi_j$ to DNF and iterate over conjunctions, looking for corresponding $u_i$ and $v_j$ for each conjunction.
You may also look at cooltt, which have some fancy way to work with faces (pay attention at these φ : 𝔽 and i=r ∨ φ).
