In the theory of types (actually I am reading mainly HoTT), or in some languages like Agda, there could be an axiom called K or something together called "reflection of identity", which cancels the type of identity / "intensional" equality.
I want to ask about the difference between Bool≡Bool and 1≡1, explaining the difference between the meaning of proposition in "propositions as types" that apparently refer to any possible type, and "mere proposition"whose member, if it is inhabited, has only one.
So under the context of sin-K:
Is 1≡1 just a "proposition", or is it more of a mere proposition?
How about Bool≡Bool? How many members do you have?
In total is Equality / type of identity Just a "proposition" or also a "mere proposition"?
I find it strange that, if 1≡1 and Bool≡Bool are considered a mere proposition, then Bool≡Bool should only have one test namely, ref, in conflict with the assumption of without K. But since the kind of equality is assumes that it is propositional equality, and the propositional type should be the mere proposition mentioned above. Have I misunderstood or missed something? Is that why other axioms should exist like the axiom of univalence?