The set of funcoids is a co-frame (without axiom of choice)

A mathematician named Todd Trimble has helped me to prove that the set of funcoids between two given sets (and more generally certain pointfree funcoids) is always a co-frame. (I knew this for funcoids but my proof required axiom of choice, while Todd’s does not require axiom of choice.)

He initially published his proof here but because his proof relies on advanced category theory I didn’t understood his proof. However Todd was so kind that he preserved me a longer more elementary version of the proof in email correspondence.

I wrote my own version of this proof in this short article which I am going to incorporate into my book.

This my proof needs some revision. Possibly I confused just join-semilattices and join-semilattices with least element are confused with each other.