daniel gratzer on Nostr: nprofile1q…4rrqe nprofile1q…a9l0g This should work I think; you are essentially ...
nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyzf5l64n2xk9azdrt6c96nwshexx45v4sduj7cyakmw005afuu05jm4rrqe (nprofile…rrqe) nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyrvy45xzsa25ave9ceu6mzf4pwfn543ad2k3l598a36e9a9wp99577a9l0g (nprofile…9l0g) This should work I think; you are essentially taking the free coproduct completion and then forcing the adjoined initial object to be the existing one. So y : C --> C+ should be universal among categories D with finite coproducts and a map F : C --> D which preserves the initial object. At least, that's a sensible universal property to describe what Reed asked for I think.