Re: [HoTT] Identity versus equality

[Michael Shulman <shu...@sandiego.edu>]

FWIW there is no trouble at all with "internal categories" in HoTT;
they just correspond to (pre)categories in the smallest universe.
Some of them will naturally be univalent categories, while others will
naturally be strict categories.  If we want to "do category theory"
with the latter we can Rezk-complete them to univalent ones, but
sometimes this is unnecessary, e.g. if our goal is to talk about
"internal presheaves" on them then these are just contravariant
functors to the (univalent) category Set, and the universal property
of Rezk-completion says that it doesn't matter whether or not we
Rezk-complete the domain before talking about presheaves.  In
addition, we get the bonus that when talking about univalent
categories internally we are externally talking about *stacks*, with
the "weak equivalences" automatically inverted (but if for some reason
we don't want to do that, we can stick with strict categories).

On Mon, May 11, 2020 at 9:37 AM <stre...@mathematik.tu-darmstadt.de> wrote:
>
> > Thank you for pointing out the case of the universe of constructible sets
> > L.
> > It is internal to ZF because it is was constructed from ordinals in ZF.
> > Could it be also external to ZF ?
>
> Anything internal can be externalized but not the other way round.
>
> The point I tried to make was that in the usual models of 2-level type
> theory the homotopical part is not internal to the ambient nonhomotopical
> part.
>
> > Gödel thought that ordinals and sets are real, like matter, but of a
> > different kind.
> > He was the first to use the full power of mathematics for studying formal
> > logic.
> > Most logicians believe that natural numbers are real.
> > They use natural numbers and induction for studying formal systems.
>
> Indeed, Goedel was the first one who took serious the difference between
> syntax and semantics. This was crucial for his findings.
> That he nevertheless was a dyed in the wool Platonist was a bit inconsequent
> but nobody is perfect :-)
>
> Thomas
>
> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyT...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/0388695a1dfc717f9c5e458937dff760.squirrel%40webmail.mathematik.tu-darmstadt.de.