I gave an online lecture about this at ItaCa on Tuesday. I am going to repeat it, again online, in the Birmingham Theoretical Computer Science seminar series. Tomorrow, Friday, 21 November at 14:00 UTC. The abstract and zoom details are at researchseminars.org/seminar/TheoryCSBham and the slides are linked from my own webpage www.paultaylor.eu/ordinals/ I will have 50 minutes instead of 30 and the reason for repeating the talk is so that people can "cross examine" me on the proof. The idea (which I have been promising for many years) for the principle "in the native language of category theory" is that there be a reflection functor from the category of well founded coalgebras to the subcategory of extensional ones. The strength of this is that it is proposed for ANY endofunctor (instead of the powerset) and ANY factorisation system (instead of plain monos), subject to some conditions. I have finally learned how ZF works and how to use it. The lecture shows that the proposal is valid in ZF. I am still working on how constructions such as transfinite iteration of functors (in particular the von Neumann hierarchy) can be obtained from my proposal. The difficulty is that the constructive categorical theory of ordinals is intrinsically a mess. (Those who have followed my work for the past 30 years will be aware that I am not saying this for want of effort in trying to sort it out.) I will give another lecture (date and venue to be decided) about this and the recovery of ZF from my proposal. ---- I would like to ask the community two questions that are relevant to this: (1) Is the General Adjoint Functor Theorem of any use? I would think that if you can find a "solution set" or any of the other possible conditions for GAFT then you should be able to describe the adjoint directly. So the interesting situation is when the adjoint has to be obtained recursively (or corecursively). This is why I think well foundedness (in some form) has to be part of the method. (2) Are there examples in the literature of category theory or algebra more generally (but not set theory) where the official first order formulation of ZF and in particular Replacement is applied? Paul Taylor You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. To take part in this conversation, reply all to this message. View group files<https://outlook.office365.com/groups/groupsubscription?source=EscalatedMessage&action=files&smtp=categories%40mq.edu.au&bO=true&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Leave group<https://outlook.office365.com/groups/groupsubscription?source=EscalatedMessage&action=leave&smtp=categories%40mq.edu.au&bO=true&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Learn more about Microsoft 365 Groups<https://aka.ms/o365g>