```------------------------------------------------------------------------
-- The Agda standard library
--
-- Algebraic properties of constructions over unary relations
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Relation.Unary.Algebra where

open import Algebra.Bundles
import Algebra.Definitions as AlgebraicDefinitions
open import Algebra.Lattice.Bundles
import Algebra.Lattice.Structures as AlgebraicLatticeStructures
import Algebra.Structures as AlgebraicStructures
open import Data.Empty.Polymorphic using (⊥-elim)
open import Data.Product.Base as Product using (_,_; proj₁; proj₂; <_,_>; curry; uncurry)
open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_])
open import Data.Unit.Polymorphic using (tt)
open import Function.Base using (id; const; _∘_)
open import Level
open import Relation.Unary hiding (∅; U)
open import Relation.Unary.Polymorphic using (∅; U)
open import Relation.Unary.Relation.Binary.Equality using (≐-isEquivalence)

module _ {a ℓ : Level} {A : Set a} where

open AlgebraicDefinitions {A = Pred A ℓ} _≐_

------------------------------------------------------------------------
-- Properties of _∩_

∩-cong : Congruent₂ _∩_
∩-cong (P⊆Q , Q⊆P) (R⊆S , S⊆R) = Product.map P⊆Q R⊆S , Product.map Q⊆P S⊆R

∩-comm : Commutative _∩_
∩-comm _ _ = Product.swap , Product.swap

∩-assoc : Associative _∩_
∩-assoc _ _ _ = Product.assocʳ′ , Product.assocˡ′

∩-idem : Idempotent _∩_
∩-idem _ = proj₁ , < id , id >

∩-identityˡ : LeftIdentity U _∩_
∩-identityˡ _ = proj₂ , < const tt , id >

∩-identityʳ : RightIdentity U _∩_
∩-identityʳ _ = proj₁ , < id , const tt >

∩-identity : Identity U _∩_
∩-identity = ∩-identityˡ , ∩-identityʳ

∩-zeroˡ : LeftZero ∅ _∩_
∩-zeroˡ _ = proj₁ , ⊥-elim

∩-zeroʳ : RightZero ∅ _∩_
∩-zeroʳ _ = proj₂ , ⊥-elim

∩-zero : Zero ∅ _∩_
∩-zero = ∩-zeroˡ , ∩-zeroʳ

------------------------------------------------------------------------
-- Properties of _∪_

∪-cong : Congruent₂ _∪_
∪-cong (P⊆Q , Q⊆P) (R⊆S , S⊆R) = Sum.map P⊆Q R⊆S , Sum.map Q⊆P S⊆R

∪-comm : Commutative _∪_
∪-comm _ _ = Sum.swap , Sum.swap

∪-assoc : Associative _∪_
∪-assoc _ _ _ = Sum.assocʳ , Sum.assocˡ

∪-idem : Idempotent _∪_
∪-idem _ = [ id , id ] , inj₁

∪-identityˡ : LeftIdentity ∅ _∪_
∪-identityˡ _ = [ ⊥-elim , id ] , inj₂

∪-identityʳ : RightIdentity ∅ _∪_
∪-identityʳ _ = [ id , ⊥-elim ] , inj₁

∪-identity : Identity ∅ _∪_
∪-identity = ∪-identityˡ , ∪-identityʳ

------------------------------------------------------------------------
-- Properties of _∩_ and _∪_

∩-distribˡ-∪ : _∩_ DistributesOverˡ _∪_
∩-distribˡ-∪ _ _ _ =
( uncurry (λ x∈P → [ inj₁ ∘ (x∈P ,_) , inj₂ ∘ (x∈P ,_) ])
, [ Product.map₂ inj₁ , Product.map₂ inj₂ ]
)

∩-distribʳ-∪ : _∩_ DistributesOverʳ _∪_
∩-distribʳ-∪ _ _ _ =
( uncurry [ curry inj₁ , curry inj₂ ]
, [ Product.map₁ inj₁ , Product.map₁ inj₂ ]
)

∩-distrib-∪ : _∩_ DistributesOver _∪_
∩-distrib-∪ = ∩-distribˡ-∪ , ∩-distribʳ-∪

∪-distribˡ-∩ : _∪_ DistributesOverˡ _∩_
∪-distribˡ-∩ _ _ _ =
( [ < inj₁ , inj₁ > , Product.map inj₂ inj₂ ]
, uncurry [ const ∘ inj₁ , (λ x∈Q → [ inj₁ , inj₂ ∘ (x∈Q ,_) ]) ]
)

∪-distribʳ-∩ : _∪_ DistributesOverʳ _∩_
∪-distribʳ-∩ _ _ _ =
( [ Product.map inj₁ inj₁ , < inj₂ , inj₂ > ]
, uncurry [ (λ x∈Q → [ inj₁ ∘ (x∈Q ,_) , inj₂ ]) , const ∘ inj₂ ]
)

∪-distrib-∩ : _∪_ DistributesOver _∩_
∪-distrib-∩ = ∪-distribˡ-∩ , ∪-distribʳ-∩

∩-abs-∪ : _∩_ Absorbs _∪_
∩-abs-∪ _ _ = proj₁ , < id , inj₁ >

∪-abs-∩ : _∪_ Absorbs _∩_
∪-abs-∩ _ _ = [ id , proj₁ ] , inj₁

∪-∩-absorptive : Absorptive _∪_ _∩_
∪-∩-absorptive = ∪-abs-∩ , ∩-abs-∪

∩-∪-absorptive : Absorptive _∩_ _∪_
∩-∪-absorptive = ∩-abs-∪ , ∪-abs-∩

module _ {a : Level} (A : Set a) (ℓ : Level) where

open AlgebraicStructures        {A = Pred A ℓ} _≐_
open AlgebraicLatticeStructures {A = Pred A ℓ} _≐_

------------------------------------------------------------------------
-- Algebraic structures of _∩_

∩-isMagma : IsMagma _∩_
∩-isMagma = record
{ isEquivalence = ≐-isEquivalence
; ∙-cong = ∩-cong
}

∩-isSemigroup : IsSemigroup _∩_
∩-isSemigroup = record
{ isMagma = ∩-isMagma
; assoc = ∩-assoc
}

∩-isBand : IsBand _∩_
∩-isBand = record
{ isSemigroup = ∩-isSemigroup
; idem = ∩-idem
}

∩-isSemilattice : IsSemilattice _∩_
∩-isSemilattice = record
{ isBand = ∩-isBand
; comm = ∩-comm
}

∩-isMonoid : IsMonoid _∩_ U
∩-isMonoid = record
{ isSemigroup = ∩-isSemigroup
; identity = ∩-identity
}

∩-isCommutativeMonoid : IsCommutativeMonoid _∩_ U
∩-isCommutativeMonoid = record
{ isMonoid = ∩-isMonoid
; comm = ∩-comm
}

∩-isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid _∩_ U
∩-isIdempotentCommutativeMonoid = record
{ isCommutativeMonoid = ∩-isCommutativeMonoid
; idem = ∩-idem
}

------------------------------------------------------------------------
-- Algebraic structures of _∪_

∪-isMagma : IsMagma _∪_
∪-isMagma = record
{ isEquivalence = ≐-isEquivalence
; ∙-cong = ∪-cong
}

∪-isSemigroup : IsSemigroup _∪_
∪-isSemigroup = record
{ isMagma = ∪-isMagma
; assoc = ∪-assoc
}

∪-isBand : IsBand _∪_
∪-isBand = record
{ isSemigroup = ∪-isSemigroup
; idem = ∪-idem
}

∪-isSemilattice : IsSemilattice _∪_
∪-isSemilattice = record
{ isBand = ∪-isBand
; comm = ∪-comm
}

∪-isMonoid : IsMonoid _∪_ ∅
∪-isMonoid = record
{ isSemigroup = ∪-isSemigroup
; identity = ∪-identity
}

∪-isCommutativeMonoid : IsCommutativeMonoid _∪_ ∅
∪-isCommutativeMonoid = record
{ isMonoid = ∪-isMonoid
; comm = ∪-comm
}

∪-isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid _∪_ ∅
∪-isIdempotentCommutativeMonoid = record
{ isCommutativeMonoid = ∪-isCommutativeMonoid
; idem = ∪-idem
}

------------------------------------------------------------------------
-- Algebraic structures of _∩_ and _∪_

∪-∩-isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero _∪_ _∩_ ∅ U
∪-∩-isSemiringWithoutAnnihilatingZero = record
{ +-isCommutativeMonoid = ∪-isCommutativeMonoid
; *-cong = ∩-cong
; *-assoc = ∩-assoc
; *-identity = ∩-identity
; distrib = ∩-distrib-∪
}

∪-∩-isSemiring : IsSemiring _∪_ _∩_ ∅ U
∪-∩-isSemiring = record
{ isSemiringWithoutAnnihilatingZero = ∪-∩-isSemiringWithoutAnnihilatingZero
; zero = ∩-zero
}

∪-∩-isCommutativeSemiring : IsCommutativeSemiring _∪_ _∩_ ∅ U
∪-∩-isCommutativeSemiring = record
{ isSemiring = ∪-∩-isSemiring
; *-comm = ∩-comm
}

∪-∩-isLattice : IsLattice _∪_ _∩_
∪-∩-isLattice = record
{ isEquivalence = ≐-isEquivalence
; ∨-comm = ∪-comm
; ∨-assoc = ∪-assoc
; ∨-cong = ∪-cong
; ∧-comm = ∩-comm
; ∧-assoc = ∩-assoc
; ∧-cong = ∩-cong
; absorptive = ∪-∩-absorptive
}

∪-∩-isDistributiveLattice : IsDistributiveLattice _∪_ _∩_
∪-∩-isDistributiveLattice = record
{ isLattice = ∪-∩-isLattice
; ∨-distrib-∧ = ∪-distrib-∩
; ∧-distrib-∨ = ∩-distrib-∪
}

∩-∪-isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero _∩_ _∪_ U ∅
∩-∪-isSemiringWithoutAnnihilatingZero = record
{ +-isCommutativeMonoid = ∩-isCommutativeMonoid
; *-cong = ∪-cong
; *-assoc = ∪-assoc
; *-identity = ∪-identity
; distrib = ∪-distrib-∩
}

------------------------------------------------------------------------
-- Algebraic bundles of _∩_

∩-magma : Magma _ _
∩-magma = record
{ isMagma = ∩-isMagma
}

∩-semigroup : Semigroup _ _
∩-semigroup = record
{ isSemigroup = ∩-isSemigroup
}

∩-band : Band _ _
∩-band = record
{ isBand = ∩-isBand
}

∩-semilattice : Semilattice _ _
∩-semilattice = record
{ isSemilattice = ∩-isSemilattice
}

∩-monoid : Monoid _ _
∩-monoid = record
{ isMonoid = ∩-isMonoid
}

∩-commutativeMonoid : CommutativeMonoid _ _
∩-commutativeMonoid = record
{ isCommutativeMonoid = ∩-isCommutativeMonoid
}

∩-idempotentCommutativeMonoid : IdempotentCommutativeMonoid _ _
∩-idempotentCommutativeMonoid = record
{ isIdempotentCommutativeMonoid = ∩-isIdempotentCommutativeMonoid
}

------------------------------------------------------------------------
-- Algebraic bundles of _∪_

∪-magma : Magma _ _
∪-magma = record
{ isMagma = ∪-isMagma
}

∪-semigroup : Semigroup _ _
∪-semigroup = record
{ isSemigroup = ∪-isSemigroup
}

∪-band : Band _ _
∪-band = record
{ isBand = ∪-isBand
}

∪-semilattice : Semilattice _ _
∪-semilattice = record
{ isSemilattice = ∪-isSemilattice
}

∪-monoid : Monoid _ _
∪-monoid = record
{ isMonoid = ∪-isMonoid
}

∪-commutativeMonoid : CommutativeMonoid _ _
∪-commutativeMonoid = record
{ isCommutativeMonoid = ∪-isCommutativeMonoid
}

∪-idempotentCommutativeMonoid : IdempotentCommutativeMonoid _ _
∪-idempotentCommutativeMonoid = record
{ isIdempotentCommutativeMonoid = ∪-isIdempotentCommutativeMonoid
}

------------------------------------------------------------------------
-- Algebraic bundles of _∩_ and _∪_

∪-∩-semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero _ _
∪-∩-semiringWithoutAnnihilatingZero = record
{ isSemiringWithoutAnnihilatingZero = ∪-∩-isSemiringWithoutAnnihilatingZero
}

∪-∩-semiring : Semiring _ _
∪-∩-semiring = record
{ isSemiring = ∪-∩-isSemiring
}

∪-∩-commutativeSemiring : CommutativeSemiring _ _
∪-∩-commutativeSemiring = record
{ isCommutativeSemiring = ∪-∩-isCommutativeSemiring
}

∪-∩-lattice : Lattice _ _
∪-∩-lattice = record
{ isLattice = ∪-∩-isLattice
}

∪-∩-distributiveLattice : DistributiveLattice _ _
∪-∩-distributiveLattice = record
{ isDistributiveLattice = ∪-∩-isDistributiveLattice
}

∩-∪-semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero _ _
∩-∪-semiringWithoutAnnihilatingZero = record
{ isSemiringWithoutAnnihilatingZero = ∩-∪-isSemiringWithoutAnnihilatingZero
}
```