Stream: Coq users

Topic: Are all terms inhabited?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Ignat Insarov (Jun 21 2022 at 07:57):

Thank you Gaëtan!

Last updated: Jun 15 2024 at 05:01 UTC