Toposes and Heyting Algebras

[FeorgeGeorge]

The proofs largely follows "Sheaves in Geometry and Logic" by Mac Lane and Moerdijk. This PR includes the following definitions and proofs:

1. Right adjoint functors with the counit and coreflection (or universal property) and a proof of uniqueness (for categories);
2. Cartesian closed precategories, exponential and exponentiable objects;
3. Product (pre)category and bifunctors: internal hom-bifunctor for CCC, binary product bifunctor for precategories with binary products;
4. Elementary topos definition;
5. Topos is cartesian closed and balanced;
6. Set topos instance;
7. Heyting algebras as cartesian closed posetal categories.
   Some supplementary lemmas about pullbacks and products were added to Limit (for example, uniqueness of pullbacks). I also suggest splitting the CartesianPrecat class in two, so that it extends precategories with a terminal object and precategories with binary products separately. This way, for example, meet-semilatice class can extend the class of precategories with binary products.

[ice1000]

What about Grothendieck topos?

[FeorgeGeorge]

When renaming this, my thinking was that the name "Elementary Topos" should be reserved for topoi with a natural numbers object, but this doesn't seem to be a common definition. Do you suggest this should be called ElementaryTopos (to distinguish it from Grothendieck topoi and others) or something else?

[ice1000]

I have no idea. I think we should ask valis. Why do you suggest E topos to be those who have an NNO? Is this a convention?

P.S. I hardly know category theory, and this might be a dumb question, don't overthink