Troncamento proposizionale del mezzo escluso

Question

Mi è chiaro che dovrebbe essere impossibile dimostrare:

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

Perché darebbe Decidere Oracle per ogni proposta.

La mia domanda riguarda i seguenti tipi:

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

o

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

Sono dimostrabili in AGDA cubica? Che cosa può dire Hott su di loro?

Tali tipi affermerebbero solo che le proposizioni sono vere o false, ma nasconderebbero informazioni sulla vera verità di A, impedendoci di costruire Oracle universale, ma permettendo, ad esempio, di fare una prova per entrambi i casi anche per proposizioni indecidibili.

La mia intuizione su tali tipi è corretta?