Propositional truncation of excluded middle

Question

It is clear to me that it should be impossible to prove :

exclMidl = isProp A → ((A) ⊎ (¬ A))

Because it would give deciding oracle for every Proposition.

My question is about the following Types:

exclMidl' = isProp A → ∥ ((A) ⊎ (¬ A)) ∥ 

or

exclMidl'' = isProp A → ∥ ((A ≡ Unit) ⊎ (A ≡ Empty)) ∥

Are they provable in cubical Agda? What HoTT can say about them?

Those types would only state that propositions are either True or False but would hide information about actual Truthness of A, preventing us from constructing universal oracle, but allowing, for example, to do a proof for both cases even for undecidable propositions.

Is my intuition about such types correct?