Proof that downset is a CCC is gross

[jacobneu]

TODO:

• Move downset construction out of CCC.lean into its own file
• Clean up proof, creating new lemmas and tactics as appropriate

[jacobneu]

Might be able to use the mathlib's implementation of Yoneda & the category of presheaves, since the downset construction is just the category of presheaves over a preorder. Likely will need to coordinate with #8 if we follow that approach