Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I added to initial object the theorem characterizing initial objects in terms of cones over the identity functor.
I drew the obvious corollary, that an object is initial iff it is the limit of the identity functor.
By the way, if I were to decide, I would replace the writeup of the proof “initial object is limit over identity functor” in the entry by what is now in Sandbox 1528 .
The existing proof was admittedly a bit telegraphic in places; I added a bit more explanation that certain triangles commute by the cone condition. But in general I like the more concise version. However, the longer version could be on a breakout subpage?
added pointer to:
Prodded by a comment here I have clarified the wording (here) regarding strict initial objects.
While I was at it I have added a bunch of Definition/Remark environments and re-arranged somewhat, for more systematics.
The remaining examples of strict initial objects I have moved to strict initial object.
1 to 9 of 9