So I'm implementing some (most of) HoTT definitions in Agda. For checking that a type is a set I have defined:
isSet : ∀ (A : Set) → Set
isSet A = ∀ {x y : A} (p q : (x ≡ y)) → (p ≡ q)
This proof that Σ(x :a) P x is a set (when the P x's are) works perfectly fine in "normal" (without importing cubical) agda:
Σ-isSet : ∀ {A : Set} (P : A → Set) → (∀ (x : A) → isSet (P x)) → isSet (∃[ z ] (P z))
Σ-isSet {A} P φ {x} {y} refl refl = refl
But when I import cubical agda (Because I need it for defining HIT), the proof doesn't work anymore:
Cannot split on argument of non-datatype x ≡ y
when checking that the pattern refl has type x ≡ y
What's happening? Is the proof incorrect, or do I need to use different operators when using cubical agda? Thank you!
The first issue is that your proof relies on axiom K and does not type-check --without-K. Axiom K essentially says that every type is a set, so it's no surprise that your lemma is trivial in that setting (notice that your proof doesn't even use the assumption φ!). Axiom K is incompatible with univalence and is therefore not assumed in HoTT.
In fact, your lemma is false in HoTT: you need both A to be a set and P to be a family of sets to conclude that Σ A P is a set. This is a good exercise: give an example of a type A and a family of sets P : A → Type such that Σ A P is not a set.
The second issue is that cubical Agda uses path types instead of inductive identity types, so you cannot pattern match on refl. Paths in A are essentially functions out of the interval type I → A with specified values at the endpoints i0 and i1. Path types support mostly the same elimination principle as the one provided by pattern matching on refl (--without-K) in the form of J, but its computation rule on refl only holds up to another path instead of definitionally.
In cubical Agda, one usually proves the more general result that Σ preserves h-levels: if A is an n-type and P is a family of n-types then Σ A P is an n-type. See 1lab or cubical for example.
As a side note, you can rename Set to Type when working with HoTT to avoid confusion:
{-# OPTIONS --no-import-sorts #-}
open import Agda.Primitive renaming (Set to Type; Setω to Typeω)
This is done for you in most cubical/HoTT libraries.