Is it the case that only types belonging to
Type are inhabited? Or are there some inhabitants for any term? For example, if I add an axiom
false: False, can I create an inhabitant of
1: nat from there? Ex falso quodlibet and all that.
only types can be inhabited
types are those terms whose type is a sort (sprop prop set type)
adding axioms creates more terms but does not change a term's type so 1 is not a type and it does not make sense to ask about it being inhabited
Thank you Gaëtan!
Last updated: Sep 30 2023 at 05:01 UTC