open import Graded.Modality
module Graded.Context.Properties.Meet
{a} {M : Set a} (𝕄 : Modality M) where
open import Graded.Context 𝕄
open import Graded.Context.Properties.Equivalence 𝕄
open import Graded.Context.Properties.PartialOrder 𝕄
open import Graded.Modality.Properties 𝕄
open import Tools.Nat using (Nat)
open Modality 𝕄
private
variable
n : Nat
γ γ′ δ δ′ η : Conₘ n
∧ᶜ-idem : (γ : Conₘ n) → γ ∧ᶜ γ ≈ᶜ γ
∧ᶜ-idem ε = ≈ᶜ-refl
∧ᶜ-idem (γ ∙ p) = (∧ᶜ-idem γ) ∙ (∧-idem p)
∧ᶜ-comm : (γ δ : Conₘ n) → γ ∧ᶜ δ ≈ᶜ δ ∧ᶜ γ
∧ᶜ-comm ε ε = ≈ᶜ-refl
∧ᶜ-comm (γ ∙ p) (δ ∙ q) = (∧ᶜ-comm γ δ) ∙ (∧-comm p q)
∧ᶜ-assoc : (γ δ η : Conₘ n) → (γ ∧ᶜ δ) ∧ᶜ η ≈ᶜ γ ∧ᶜ (δ ∧ᶜ η)
∧ᶜ-assoc ε ε ε = ≈ᶜ-refl
∧ᶜ-assoc (γ ∙ p) (δ ∙ q) (η ∙ r) = (∧ᶜ-assoc γ δ η) ∙ (∧-assoc p q r)
∧ᶜ-cong : γ ≈ᶜ γ′ → δ ≈ᶜ δ′ → γ ∧ᶜ δ ≈ᶜ γ′ ∧ᶜ δ′
∧ᶜ-cong ε ε = ≈ᶜ-refl
∧ᶜ-cong (γ≈ᶜγ′ ∙ p≡p′) (δ≈ᶜδ′ ∙ q≡q′) =
∧ᶜ-cong γ≈ᶜγ′ δ≈ᶜδ′ ∙ ∧-cong p≡p′ q≡q′
∧ᶜ-congˡ : δ ≈ᶜ δ′ → γ ∧ᶜ δ ≈ᶜ γ ∧ᶜ δ′
∧ᶜ-congˡ δ≈ᶜδ′ = ∧ᶜ-cong ≈ᶜ-refl δ≈ᶜδ′
∧ᶜ-congʳ : γ ≈ᶜ γ′ → γ ∧ᶜ δ ≈ᶜ γ′ ∧ᶜ δ
∧ᶜ-congʳ γ≈ᶜγ′ = ∧ᶜ-cong γ≈ᶜγ′ ≈ᶜ-refl
∧ᶜ-monotoneˡ : γ ≤ᶜ δ → γ ∧ᶜ η ≤ᶜ δ ∧ᶜ η
∧ᶜ-monotoneˡ {γ = ε} {ε} {ε} ε = ≤ᶜ-refl
∧ᶜ-monotoneˡ {γ = γ ∙ p} {δ ∙ q} {η ∙ r} (γ≤δ ∙ p≤q) =
(∧ᶜ-monotoneˡ γ≤δ) ∙ (∧-monotoneˡ p≤q)
∧ᶜ-monotoneʳ : γ ≤ᶜ δ → η ∧ᶜ γ ≤ᶜ η ∧ᶜ δ
∧ᶜ-monotoneʳ {γ = ε} {ε} {ε} ̋ε = ≤ᶜ-refl
∧ᶜ-monotoneʳ {γ = γ ∙ p} {δ ∙ q} {η ∙ r} (γ≤δ ∙ p≤q) =
(∧ᶜ-monotoneʳ γ≤δ) ∙ (∧-monotoneʳ p≤q)
∧ᶜ-monotone : γ ≤ᶜ γ′ → δ ≤ᶜ δ′ → (γ ∧ᶜ δ) ≤ᶜ (γ′ ∧ᶜ δ′)
∧ᶜ-monotone γ≤γ′ δ≤δ′ = ≤ᶜ-trans (∧ᶜ-monotoneˡ γ≤γ′) (∧ᶜ-monotoneʳ δ≤δ′)
∧ᶜ-decreasingˡ : (γ δ : Conₘ n) → γ ∧ᶜ δ ≤ᶜ γ
∧ᶜ-decreasingˡ ε ε = ≤ᶜ-refl
∧ᶜ-decreasingˡ (γ ∙ p) (δ ∙ q) = (∧ᶜ-decreasingˡ γ δ) ∙ (∧-decreasingˡ p q)
∧ᶜ-decreasingʳ : (γ δ : Conₘ n) → γ ∧ᶜ δ ≤ᶜ δ
∧ᶜ-decreasingʳ ε ε = ≤ᶜ-refl
∧ᶜ-decreasingʳ (γ ∙ p) (δ ∙ q) = (∧ᶜ-decreasingʳ γ δ) ∙ (∧-decreasingʳ p q)
∧ᶜ-greatest-lower-bound : γ ≤ᶜ δ → γ ≤ᶜ η → γ ≤ᶜ δ ∧ᶜ η
∧ᶜ-greatest-lower-bound {γ = ε} {δ = ε} {η = ε} ε ε =
ε
∧ᶜ-greatest-lower-bound
{γ = _ ∙ _} {δ = _ ∙ _} {η = _ ∙ _} (γ≤δ ∙ p≤q) (γ≤η ∙ p≤r) =
∧ᶜ-greatest-lower-bound γ≤δ γ≤η ∙ ∧-greatest-lower-bound p≤q p≤r
+ᶜ≤ᶜ∧ᶜ :
(∀ p q → p + q ≤ p ∧ q) →
γ +ᶜ δ ≤ᶜ γ ∧ᶜ δ
+ᶜ≤ᶜ∧ᶜ {γ = ε} {δ = ε} _ = ε
+ᶜ≤ᶜ∧ᶜ {γ = _ ∙ _} {δ = _ ∙ _} +≤∧ = +ᶜ≤ᶜ∧ᶜ +≤∧ ∙ +≤∧ _ _
∧ᶜ≤ᶜ+ᶜ :
(∀ p q → p ∧ q ≤ p + q) →
γ ∧ᶜ δ ≤ᶜ γ +ᶜ δ
∧ᶜ≤ᶜ+ᶜ {γ = ε} {δ = ε} _ = ε
∧ᶜ≤ᶜ+ᶜ {γ = _ ∙ _} {δ = _ ∙ _} ∧≤+ = ∧ᶜ≤ᶜ+ᶜ ∧≤+ ∙ ∧≤+ _ _