Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeSep 20th 2012
   • (edited Sep 20th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexWhen I made _[[inhabitant]]_ redirect to _[[term]]_ a few minutes ago, I noticed a bunch of orphaned related entries. For instance _[[inhabited type]]_ since long ago redirect to _[[inhabited set]]_. I haven't changed that yet, but I added some cross links and comments to make clear that and how the three * [[inhabited type]] * [[inhabited object]], [[inhabited set]] are related. The state of these entries deserves to be improved on, but I won't do anything further right now.

   When I made inhabitant redirect to term a few minutes ago, I noticed a bunch of orphaned related entries.

   For instance inhabited type since long ago redirect to inhabited set. I haven’t changed that yet, but I added some cross links and comments to make clear that and how the three

   • inhabited type

     • inhabited object, inhabited set

   are related. The state of these entries deserves to be improved on, but I won’t do anything further right now.

2. • CommentRowNumber2.
   • CommentAuthorTobyBartels
   • CommentTimeSep 21st 2012
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexBut [[inhabitant]] doesn't redirect to [[term]]; in fact, [[inhabitant]] redirects nowhere, and nothing (except the plural) redirects to [[term]]. Should I fix that, or did you change your mind?

   But inhabitant doesn’t redirect to term; in fact, inhabitant redirects nowhere, and nothing (except the plural) redirects to term.

   Should I fix that, or did you change your mind?

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeSep 21st 2012
   • (edited Sep 21st 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexWoops. Thanks for catching that. Not sure what happened there. I did mean to have both [[inhabitant]] and [[inhabitants]] redirect to [[term]]. Did that now. But let me know if you think it should have an entry of its own.

   Woops. Thanks for catching that. Not sure what happened there. I did mean to have both inhabitant and inhabitants redirect to term. Did that now.

   But let me know if you think it should have an entry of its own.

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeDec 29th 2016
   • (edited Dec 29th 2016)
   • PermaLink
   Author: Urs
   Format: MarkdownItexSomebody with a spare minute should please fix _[[inhabited type]]_: it fails to properly discuss the distinction between a type $X$ admitting a term, and its propositional truncation $\Vert X \Vert$ admitting a term.

   Somebody with a spare minute should please fix inhabited type: it fails to properly discuss the distinction between a type $X$ admitting a term, and its propositional truncation $\Vert X \Vert$ admitting a term.

5. • CommentRowNumber5.
   • CommentAuthorTodd_Trimble
   • CommentTimeDec 29th 2016
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexI made a slight amendment to the opening paragraph, which is parallel, but I prefer that someone more immersed in type theory do the honors re propositional truncation.

   I made a slight amendment to the opening paragraph, which is parallel, but I prefer that someone more immersed in type theory do the honors re propositional truncation.

6. • CommentRowNumber6.
   • CommentAuthorDavid_Corfield
   • CommentTimeDec 29th 2016
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexIs the redirect to 'inhabited set' ideal?

   Is the redirect to ’inhabited set’ ideal?

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeDec 29th 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexPersonally, I would make "inhabitant" redirect to [[element]]; to me a "term" is a much more syntactic thing.

   Personally, I would make “inhabitant” redirect to element; to me a “term” is a much more syntactic thing.

8. • CommentRowNumber8.
   • CommentAuthorMike Shulman
   • CommentTimeDec 29th 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI tried to clean up the discussions of the two kinds of inhabitation, in particular moving the theorem about well-pointed toposes from [[inhabited set]] to [[inhabited object]].

   I tried to clean up the discussions of the two kinds of inhabitation, in particular moving the theorem about well-pointed toposes from inhabited set to inhabited object.

9. • CommentRowNumber9.
   • CommentAuthorUrs
   • CommentTimeDec 30th 2016
   • PermaLink
   Author: Urs
   Format: MarkdownItexThanks!

   Thanks!