Cubical Agda

Cubical Agda is an implementation of cubical type theory as an Agda extension, but may as well be thought of as a separate language. It's very different and very incompatible with non-cubical Agda.

isProp

A type is a proposition if it is "proof-irrelevant" — if all proofs of A are equivalent.

From the 1Lab:

At this point, we should introduce the proper terminology, rather than speaking of “proving” types and “constructing” types. We say that a type $T$ is a proposition, written is-prop below, if any two of its inhabitants are identified. Since every construction is invariant under identifications (by definition), this means that any two putative constructions $\mathrm{Type}x,yT$ are indistinguishable — they’re really the same proof.

[cite:@1lab]

isProp : Type ℓ → Type ℓ
isProp A = (x y : A) → x ≡ y

isSet

From the 1Lab:

Knowing about propositions, we can now rephrase our earlier statement about the natural numbers: each identity type $x{\equiv }_{\mathbb{N}}y$ is a proposition. Types for which this statement holds are called sets. A proof that a type $T$ is a set is a licence to stop caring about how we show that $\mathrm{Type}x,yT$ are identified — we even say that they’re just equal.

[cite:@1lab]

isSet : Type ℓ → Type ℓ
isSet A = (x y : A) → isProp (x ≡ y)

hSet

A pair $(T,\text{𝚒𝚜𝚂𝚎𝚝}T)$.