DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Add associativity proofs

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin
2026-02-14 13:47:39 -08:00
parent ccc3c7d5c7
commit c6e525ad7c
1 changed files with 26 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

26
Lattice/Builder.agda
View File

@@ -543,3 +543,29 @@ record Graph : Set where
with (n₂₁ , ((n₂→n₂n₁ , n₁→n₂n₁) , n₂→n'×n₁→n'⇒n₂₁→n')) ← total-⊓ n₂ n₁
= n₁→n₂×n₂→n₁⇒n₁≡n₂ (n₁→n'×n₂→n'⇒n₁₂→n' n₂₁ (n₁→n₂n₁ , n₂→n₂n₁))
(n₂→n'×n₁→n'⇒n₂₁→n' n₁₂ (n₂→n₁n₂ , n₁→n₁n₂))
⊔-assoc : ∀ n₁ n₂ n₃ → (n₁ ⊔ n₂) ⊔ n₃ ≡ n₁ ⊔ (n₂ ⊔ n₃)
⊔-assoc n₁ n₂ n₃
with (n₁₂ , ((n₁₂→n₁ , n₁₂→n₂) , n'→n₁×n'→n₂⇒n'→n₁₂)) ← total-⊔ n₁ n₂
with (n₁₂,₃ , ((n₁₂,₃→n₁₂ , n₁₂,₃→n₃) , n'→n₁₂×n'→n₃⇒n'→n₁₂,₃)) ← total-⊔ n₁₂ n₃
with (n₂₃ , ((n₂₃→n₂ , n₂₃→n₃) , n'→n₂×n'→n₃⇒n'→n₂₃)) ← total-⊔ n₂ n₃
with (n₁,₂₃ , ((n₁,₂₃→n₁ , n₁,₂₃→n₂₃) , n'→n₁×n'→n₂₃⇒n'→n₁,₂₃)) ← total-⊔ n₁ n₂₃
=
let n₁₂,₃→n₂₃ = n'→n₂×n'→n₃⇒n'→n₂₃ n₁₂,₃ (n₁₂,₃→n₁₂ ++ n₁₂→n₂ , n₁₂,₃→n₃)
n₁₂,₃→n₁,₂₃ = n'→n₁×n'→n₂₃⇒n'→n₁,₂₃ n₁₂,₃ (n₁₂,₃→n₁₂ ++ n₁₂→n₁ , n₁₂,₃→n₂₃)
n₁,₂₃→n₁₂ = n'→n₁×n'→n₂⇒n'→n₁₂ n₁,₂₃ (n₁,₂₃→n₁ , n₁,₂₃→n₂₃ ++ n₂₃→n₂)
n₁,₂₃→n₁₂,₃ = n'→n₁₂×n'→n₃⇒n'→n₁₂,₃ n₁,₂₃ (n₁,₂₃→n₁₂ , n₁,₂₃→n₂₃ ++ n₂₃→n₃)
in n₁→n₂×n₂→n₁⇒n₁≡n₂ n₁₂,₃→n₁,₂₃ n₁,₂₃→n₁₂,₃
⊓-assoc : ∀ n₁ n₂ n₃ → (n₁ ⊓ n₂) ⊓ n₃ ≡ n₁ ⊓ (n₂ ⊓ n₃)
⊓-assoc n₁ n₂ n₃
with (n₁₂ , ((n₁→n₁₂ , n₂→n₁₂) , n₁→n'×n₂→n'⇒n₁₂→n')) ← total-⊓ n₁ n₂
with (n₁₂,₃ , ((n₁₂→n₁₂,₃ , n₃→n₁₂,₃) , n₁₂→n'×n₃→n'⇒n₁₂,₃→n')) ← total-⊓ n₁₂ n₃
with (n₂₃ , ((n₂→n₂₃ , n₃→n₂₃) , n₂→n'×n₃→n'⇒n₂₃→n')) ← total-⊓ n₂ n₃
with (n₁,₂₃ , ((n₁→n₁,₂₃ , n₂₃→n₁,₂₃) , n₁→n'×n₂₃→n'⇒n₁,₂₃→n')) ← total-⊓ n₁ n₂₃
=
let n₁₂→n₁,₂₃ = n₁→n'×n₂→n'⇒n₁₂→n' n₁,₂₃ (n₁→n₁,₂₃ , n₂→n₂₃ ++ n₂₃→n₁,₂₃)
n₁₂,₃→n₁,₂₃ = n₁₂→n'×n₃→n'⇒n₁₂,₃→n' n₁,₂₃ (n₁₂→n₁,₂₃ , n₃→n₂₃ ++ n₂₃→n₁,₂₃)
n₂₃→n₁₂,₃ = n₂→n'×n₃→n'⇒n₂₃→n' n₁₂,₃ (n₂→n₁₂ ++ n₁₂→n₁₂,₃ , n₃→n₁₂,₃)
n₁,₂₃→n₁₂,₃ = n₁→n'×n₂₃→n'⇒n₁,₂₃→n' n₁₂,₃ (n₁→n₁₂ ++ n₁₂→n₁₂,₃ , n₂₃→n₁₂,₃)
in n₁→n₂×n₂→n₁⇒n₁≡n₂ n₁₂,₃→n₁,₂₃ n₁,₂₃→n₁₂,₃