From b6b7ac4b8c258846edc96655292e20fc6c83109c Mon Sep 17 00:00:00 2001 From: James Henri Haydon Date: Sun, 6 Jul 2025 17:46:39 +0900 Subject: [PATCH] feat: products of Heyting algebras Heyting algebras are stable under cartesian product. A reference is here: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Heyting/Basic.html#Prod.instHeytingAlgebra --- src/Algebra/Heyting.hs | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/Algebra/Heyting.hs b/src/Algebra/Heyting.hs index 5a49637..599c2e2 100644 --- a/src/Algebra/Heyting.hs +++ b/src/Algebra/Heyting.hs @@ -91,6 +91,11 @@ instance Heyting a => Heyting (b -> a) where f <=> g = \x -> f x <=> g x neg f = neg . f +instance (Heyting a, Heyting b) => Heyting (a, b) where + (a1, b1) ==> (a2, b2) = (a1 ==> a2, b1 ==> b2) + neg (a, b) = (neg a, neg b) + (a1, b1) <=> (a2, b2) = (a1 <=> a2, b1 <=> b2) + ------------------------------------------------------------------------------- -- All, Any, Endo -------------------------------------------------------------------------------