What does "no axioms" really mean?

Stream: new members

[David Michael Roberts]

Someone on mathstodon formalised my minimalist version of Lawvere's Fixed Point Theorem:

https://mathstodon.xyz/@highergeometer/112098277610968736

and while I'm fully aware that when #print axioms says that it "does not depend on any axioms" that is a slight lie-to-children, what does it "really" mean? This is obviously only a shallow embedding, it's not for arbitrary magmoidal categories with diagonals.

[Ruben Van de Velde]

That it doesn't depend on choice, mostly

[Floris van Doorn]

that it only depends on the bare rules of the type theory. You can find these in chapters 2 and 7 of #tpil. Chapter 12 is about the axioms.