arend-lib
arend-lib copied to clipboard
JetBrains
Definition of a Heyting algebra together with the adjunction + the (- x A) functor for cartesian categories
https://github.com/JetBrains/arend-lib/blob/d37974021d69917ef04f034c954a801e0de64223/src/Logic/Classical.ard#L26 lmfao
in src/Category.ard instead of | \fixl 8 o \alias \infixl 8 ∘ {X Y Z : Ob} : Hom Y Z -> Hom X Y -> Hom X Z make...
There are several goals left in [Arith.Real](https://github.com/JetBrains/arend-lib/blob/b05bc6a39e24c4230e308f5c88f7b93023c21246/src/Arith/Real.ard): - [ ] The locatedness property for the product of two reals. - [ ] The locatedness property for the inverse of a...
Meta `equation` finds the first appropriate instance, but it might not be the best. For example, it could use an instance of the Ring class instead of CRing if the...
This is [Topology.Locale/wregular_wHausdorff](https://github.com/JetBrains/arend-lib/blob/4ea97da483c5bb2e6a22c8d09c03becf17756c7e/src/Topology/Locale.ard#L1364). A proof of this proposition can be found in Fibrewise separation axioms for locales, Peter T. Johnstone, 1990, Corollary 3.4. This proposition requires a lot of background...
This is [Topology.Locale/open-comp](https://github.com/JetBrains/arend-lib/blob/4ea97da483c5bb2e6a22c8d09c03becf17756c7e/src/Topology/Locale.ard#L1194). A proof of this proposition can be found in Handbook of Categorical Algebra: Volume 3, Francis Borceux, 1994 (Chapter 1), Corollary 1.6.3.