search

JetBrains / arend-lib

Apache License 2.0
79 stars 23 forks source link

Toposes and Heyting Algebras #64

Closed FeorgeGeorge closed 4 months ago

FeorgeGeorge commented 7 months ago

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.