Ignat Insarov (Jun 20 2022 at 19:03): Ignat Insarov (Jun 20 2022 at 19:03):Is it the case that only types belonging to Set, Prop or 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.
Gaëtan Gilbert (Jun 20 2022 at 19:55):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
Ignat Insarov (Jun 21 2022 at 07:57):Thank you Gaëtan!
Last updated: Oct 13 2024 at 01:02 UTC