I am taking the liberty of truncating the title from *semantics of Set in homotopy type theory* to *Set in homotopy type theory*.

Besides better matching the corresponding entry *Set*, and being less bulky as a title, this matches the title of the single reference that is given, and is not as directly in conflict with the idea offered in the Idea-section.

The first sentence does not type-check:

Sets in homotopy type theory behave a lot like the internal language of a topos.

What you mean is something like:

]]>The syntax for sets in homotopy type theory behaves a lot like the internal language of a topos.

copying article from HoTT wiki

Anonymous

]]>