Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Relations form a semiring!
-- 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₂))
}
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.