Simplify Embedding-into-hLevel→hLevel

[MatthiasHu]

This small PR simplifies the proofs of Embedding-into-hLevel→hLevel and the two special cases for isProp and isSet.

Embedding-into-hLevel→hLevel was unnecessarily defined by case distinction. The reason is probably the definition of isOfHLevel by three instead of two cases:

cubical/Cubical/Foundations/HLevels.agda

Lines 44 to 47 in a10e25a

	isOfHLevel : HLevel → Type ℓ → Type ℓ
	isOfHLevel 0 A = isContr A
	isOfHLevel 1 A = isProp A
	isOfHLevel (suc (suc n)) A = (x y : A) → isOfHLevel (suc n) (x ≡ y)

I assume there are good reasons for this definition of isOfHLevel, but I suppose it was not intended to spark unnecessary case distinctions in places like Embedding-into-hLevel→hLevel.

[mortberg]

I have no clue why this was so complicated and I like the new simpler version. Maybe @aljungstrom knows more? (It could have had something to do with attempts to optimize things...)

[felixwellen]

Does not take longer than usual to type check on my machine. So there can't be any dramatic efficiency difference.

[felixwellen]

Ahno, now I get it. You did not change the definition of isOfHLevel.

[felixwellen]

I would guess that is just about having definitional equalities between isOfHLevel 0 and isContr and isOfHLevel 1 and isProp, where isContr and isProp are defined like in the HoTT-Book. isSet then also fits in definitionally.

[MatthiasHu]

You did not change the definition of isOfHLevel.

Correct.

The three-cases definition of isOfHLevel was introduced and discussed here: #68