Relations form a semiring!

Relations.agda

-- See also https://gist.github.com/copumpkin/2636229
module Relations where

open import Level
open import Function
open import Algebra
open import Data.Empty
open import Data.Sum as Sum
open import Data.Product as Prod
open import Relation.Binary
open import Relation.Binary.PropositionalEquality hiding (isEquivalence)

record Iso {i ℓ ℓ′} {I : Set i} (A : Rel I ℓ) (B : Rel I ℓ′) : Set (ℓ ⊔ ℓ′ ⊔ i) where
  constructor iso
  field
    to   : ∀ {i j} → A i j → B i j
    from : ∀ {i j} → B i j → A i j
    p : ∀ {i j} (x : B i j) → to (from x) ≡ x
    p′ : ∀ {i j} (x : A i j) → from (to x) ≡ x

isEquivalence : ∀ {ℓ i} {I : Set i} → IsEquivalence (Iso {ℓ = ℓ} {I = I})
isEquivalence {ℓ} {i} {I} = record
  { refl = iso id id (λ _ → refl) (λ _ → refl)
  ; sym = λ { (iso to from p p′) → iso from to p′ p }
  ; trans = trans′
  }
  where
  trans′ : ∀ {A B C : Rel I ℓ} → Iso A B → Iso B C → Iso A C
  trans′ {A} {B} {C} (iso to₁ from₁ p₁ p′₁) (iso to₂ from₂ p₂ p′₂) = iso (to₂ ∘ to₁) (from₁ ∘′ from₂) pf pf′
    where
    pf : ∀ {i j} (x : C i j) → to₂ (to₁ (from₁ (from₂ x))) ≡ x
    pf x rewrite p₁ (from₂ x) = p₂ x
 
    pf′ : ∀ {i j} (x : A i j) → from₁ (from₂ (to₂ (to₁ x))) ≡ x
    pf′ x rewrite p′₂ (to₁ x) = p′₁ x

_⊕_ : ∀ {i ℓ} {I : Set i} → Rel I ℓ → Rel I ℓ → Rel I ℓ
A ⊕ B = λ i j → A i j ⊎ B i j

⊕-cong : ∀ {i ℓ} {I : Set i} {A B C D : Rel I ℓ} → Iso A B → Iso C D → Iso (A ⊕ C) (B ⊕ D)
⊕-cong (iso to from p p′) (iso to₁ from₁ p₁ p′₁)
  = iso (Sum.map to to₁)
        (Sum.map from from₁)
        (λ { (inj₁ y) → cong inj₁ (p y); (inj₂ v) → cong inj₂ (p₁ v) })
        (λ { (inj₁ x) → cong inj₁ (p′ x); (inj₂ u) → cong inj₂ (p′₁ u) })

_⊗_ : ∀ {i ℓ} {I : Set i} → Rel I ℓ → Rel I ℓ → Rel I (ℓ ⊔ i)
A ⊗ B = λ i k → ∃ (λ j → A i j × B j k)

⊗-cong : ∀ {i ℓ} {I : Set i} {A B C D : Rel I ℓ} → Iso A B → Iso C D → Iso (A ⊗ C) (B ⊗ D)
⊗-cong {A = A} {B} {C} {D} (iso to from p p′) (iso to₁ from₁ p₁ p′₁)
  = iso (λ { (i , x , y) → i , to x , to₁ y })
        (λ { (i , x , y) → i , from x , from₁ y })
        pf pf′
  where
  pf : ∀ {i j} (x : (B ⊗ D) i j) → (proj₁ x , to (from (proj₁ (proj₂ x))) , to₁ (from₁ (proj₂ (proj₂ x)))) ≡ x
  pf (_ , x , y) rewrite p x | p₁ y = refl
 
  pf′ : ∀ {i j} (x : (A ⊗ C) i j) → (proj₁ x , from (to (proj₁ (proj₂ x))) , from₁ (to₁ (proj₂ (proj₂ x)))) ≡ x
  pf′ (_ , x , y) rewrite p′ x | p′₁ y = refl


Id : ∀ ℓ {i} {I : Set i} → Rel I (ℓ ⊔ i)
Id ℓ = λ i j → Lift {ℓ = ℓ} (i ≡ j)

idˡ : ∀ {ℓ i} {I : Set i} (q : Rel I (ℓ ⊔ i))  → Iso (Id ℓ ⊗ q) q
idˡ {ℓ} q = iso to (λ x → _ , lift refl , x) (λ _ → refl) pf
  where
  to : ∀ {i j} → (Id ℓ ⊗ q) i j → q i j
  to (i , lift refl , x) = x

  pf : ∀ {i j} → (x : (Id ℓ ⊗ q) i j) → (i , lift refl , to x) ≡ x
  pf (i , lift refl , x) = refl

idʳ : ∀ {ℓ i} {I : Set i} (q : Rel I (ℓ ⊔ i))  → Iso (q ⊗ Id ℓ) q
idʳ {ℓ} q = iso to (λ x → _ , x , lift refl) (λ _ → refl) pf
  where
  to : ∀ {i j} → (q ⊗ Id ℓ) i j → q i j
  to (i , x , lift refl) = x

  pf : ∀ {i j} → (x : (q ⊗ Id ℓ) i j) → (j , to x , lift refl) ≡ x
  pf (i , x , lift refl) = refl


semiring : ∀ {i} ℓ → Set i → Semiring (suc ℓ ⊔ suc i) (ℓ ⊔ i)
semiring {i} ℓ I = record
  { Carrier = Rel I (ℓ ⊔ i)
  ; _≈_ = Iso
  ; _+_ = _⊕_
  ; _*_ = _⊗_
  ; 0# = λ i j → Lift ⊥
  ; 1# = Id ℓ
  ; isSemiring = record
    { isSemiringWithoutAnnihilatingZero = record
      { +-isCommutativeMonoid = record
        { isSemigroup = record
          { isEquivalence = isEquivalence
          ; assoc = λ _ _ _ → iso [ [ inj₁ , inj₂ ∘ inj₁ ]′ , inj₂ ∘ inj₂ ]′
                                  [ inj₁ ∘ inj₁ , [ inj₁ ∘ inj₂ , inj₂ ]′ ]′
                                  (λ { (inj₁ _) → refl; (inj₂ (inj₁ _)) → refl; (inj₂ (inj₂ _)) → refl })
                                  (λ { (inj₁ (inj₁ _)) → refl; (inj₁ (inj₂ _)) → refl; (inj₂ _) → refl })
          ; ∙-cong = ⊕-cong
          }
        ; identityˡ = λ _ → iso [ ⊥-elim ∘ lower , id ]′ inj₂ (λ _ → refl) λ { (inj₁ abs) → ⊥-elim (lower abs); (inj₂ x) → refl }
        ; comm = λ _ _ → iso [ inj₂ , inj₁ ]′ [ inj₂ , inj₁ ]′ (λ { (inj₁ y) → refl ; (inj₂ x) → refl }) (λ { (inj₁ x) → refl ; (inj₂ y) → refl })
        }
      ; *-isMonoid = record
        { isSemigroup = record
          { isEquivalence = isEquivalence
          ; assoc = λ _ _ _ → iso (λ { (j , (j′ , x , y) , z) → j′ , x , (j , y , z) })
                                  (λ { (j , x , (j′ , y , z)) → j′ , (j , x , y) , z })
                                  (λ _ → refl) (λ _ → refl)
          ; ∙-cong = ⊗-cong
          }
        ; identity = idˡ , idʳ
        }
        
      ; distrib = (λ _ _ _ → iso (λ { (i , x , inj₁ y) → inj₁ (i , x , y); (i , x , inj₂ y) → inj₂ (i , x , y) })
                                 (λ { (inj₁ (i , x , y)) → i , x , inj₁ y; (inj₂ (i , x , y)) → i , x , inj₂ y })
                                 (λ { (inj₁ _) → refl; (inj₂ _) → refl })
                                 (λ { (_ , _ , inj₁ _) → refl; (_ , _ , inj₂ _) → refl }))
                , (λ _ _ _ → iso (λ { (i , inj₁ x , y) → inj₁ (i , x , y); (i , inj₂ x , y) → inj₂ (i , x , y) })
                                 (λ { (inj₁ (i , x , y)) → i , inj₁ x , y; (inj₂ (i , x , y)) → i , inj₂ x , y })
                                 (λ { (inj₁ _) → refl; (inj₂ _) → refl })
                                 (λ { (_ , inj₁ _ , _) → refl; (_ , inj₂ _ , _) → refl }))
    }
    ; zero = (λ _ → iso (proj₁ ∘ proj₂) (⊥-elim ∘ lower) (⊥-elim ∘ lower) (⊥-elim ∘ lower ∘ proj₁ ∘ proj₂))
           , (λ _ → iso (proj₂ ∘ proj₂) (⊥-elim ∘ lower) (⊥-elim ∘ lower) (⊥-elim ∘ lower ∘ proj₂ ∘ proj₂))
    }
  }