From 0ba4b46e168f52e496874ff3f93019ac83149579 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 11 Feb 2024 15:35:50 -0800 Subject: [PATCH] Add proof of decidable equivalence for products Signed-off-by: Danila Fedorin --- Lattice/Prod.agda | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/Lattice/Prod.agda b/Lattice/Prod.agda index 7dc79d7..95a901f 100644 --- a/Lattice/Prod.agda +++ b/Lattice/Prod.agda @@ -94,6 +94,16 @@ isLattice = record ) } + +module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) where + ≈-dec : IsDecidable _≈_ + ≈-dec (a₁ , b₁) (a₂ , b₂) + with ≈₁-dec a₁ a₂ | ≈₂-dec b₁ b₂ + ... | yes a₁≈a₂ | yes b₁≈b₂ = yes (a₁≈a₂ , b₁≈b₂) + ... | no a₁̷≈a₂ | _ = no (λ (a₁≈a₂ , _) → a₁̷≈a₂ a₁≈a₂) + ... | _ | no b₁̷≈b₂ = no (λ (_ , b₁≈b₂) → b₁̷≈b₂ b₁≈b₂) + + module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) (h₁ h₂ : ℕ) (fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where