experiments with partial functions in cubical Agda