Hello. I'd like to see if I have the situation straight:

For presenting a topos as a type system, there are expected to be (at least) two styles: having a type of "static" propositions, or using hprops.

With hprops, you can prove unique choice, so it's always topos-like (pretopos?).

With static props, you can't prove unique choice, but it may be consistent as an additional primitive, or you can ensure in some other way that you have a subobject classifier.

If you don't necessarily have unique choice or equivalent, you're dealing with a quasitopos, which is a more general thing.

With static props and unique choice, subsingletons generally aren't already propositions, but they all correspond to a proposition stating that the subsingleton is inhabited. Unique choice obtains the element of a subsingleton known to be inhabited.

The usual way to present a topos as a type system is with a non-dependent type system like IHOL. This will not be able to express hprops, so static props is the way. Proofs will not be objects, so proof-irrelevance doesn't come up.

The static props approach can also be used in a dependent type system, along with unique choice or equivalent. (To say nothing of whether that's a natural kind of system.)

In a dependent type system, a type of static props may or may not be a universe.

If it's not, proofs still aren't objects and proof-irrelevance still doesn't come up.

But if it is, you should at least have typal proof-irrelevance. (That is, stated using equality types.)

In that case, with equality reflection, you automatically get judgmental proof-irrelevance. This does not necessarily mean that proofs are computationally irrelevant. With unique choice, they cannot be, or else you lose canonicity.

All OK?