Two iset.mm theorems related to truth values

[jkingdon]

The two theorems here are:

• Given a condition called the uniformity principle (which I gather is satisfied by a realizability topos, although that part is outside what we can express in iset.mm), the power set of a singleton is not countable (using the usual iset.mm definition of countability). This is an exercise from Andrej Bauer and I formalized the solution of Rahul Chhabra - see thread at https://mathstodon.xyz/@andrejbauer/112462518974897104
• 𝐴 ⊆ {𝐵} → ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 𝑦 = 𝑧 . This is very loosely based on the discussion of hProp and related topics at https://proofassistants.stackexchange.com/questions/1774/when-is-hprop-equivalent-to-the-subobject-classifier but again this is not a full treatment of the subject just one result we readily can prove in iset.mm.

[jkingdon]

It's really nice to see how to can immediately translate those Mastodon discussions!

Some of the discussions!

There are several people there who have been doing a good job posting exercises in constructive mathematics which make good attainable iset.mm proofs.