Types form a commutative semiring!

Types.agda

module Types where

open import Level
open import Function
open import Algebra
open import Data.Empty
open import Data.Unit
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 {ℓ ℓ′} (A : Set ℓ) (B : Set ℓ′) : Set (ℓ ⊔ ℓ′) where
  constructor iso
  field
    to   : A → B
    from : B → A
    p : ∀ x → to (from x) ≡ x
    p′ : ∀ x → from (to x) ≡ x

isEquivalence : ∀ {ℓ} → IsEquivalence {suc ℓ} Iso
isEquivalence {ℓ} = 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 : Set ℓ} → Iso a b → Iso b c → Iso a c
  trans′ (iso to₁ from₁ p₁ p′₁) (iso to₂ from₂ p₂ p′₂) = iso (to₂ ∘ to₁) (from₁ ∘′ from₂) pf pf′
    where
    pf : ∀ x → to₂ (to₁ (from₁ (from₂ x))) ≡ x
    pf x rewrite p₁ (from₂ x) = p₂ x

    pf′ : ∀ x → from₁ (from₂ (to₂ (to₁ x))) ≡ x
    pf′ x rewrite p′₂ (to₁ x) = p′₁ x

⊎-cong : ∀ {ℓ} {x y u v : Set ℓ} → Iso x y → Iso u v → Iso (x ⊎ u) (y ⊎ v)
⊎-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) })

×-cong : ∀ {ℓ} {x y u v : Set ℓ} → Iso x y → Iso u v → Iso (x × u) (y × v)
×-cong (iso to from p p′) (iso to₁ from₁ p₁ p′₁) 
  = iso (Prod.map to to₁)
        (Prod.map from from₁)
        pf
        pf′
  where
  pf : ∀ x → (to (from (proj₁ x)) , to₁ (from₁ (proj₂ x))) ≡ x
  pf (x , y) rewrite p x | p₁ y = refl

  pf′ : ∀ x → (from (to (proj₁ x)) , from₁ (to₁ (proj₂ x))) ≡ x
  pf′ (x , y) rewrite p′ x | p′₁ y = refl

commutativeSemiring : (ℓ : Level) → CommutativeSemiring (suc ℓ) ℓ
commutativeSemiring ℓ = record 
  { Carrier = Set ℓ
  ; _≈_ = Iso
  ; _+_ = _⊎_
  ; _*_ = _×_
  ; 0# = Lift ⊥
  ; 1# = Lift ⊤
  ; isCommutativeSemiring = record 
    { +-isCommutativeMonoid = record 
      { isSemigroup = record
        { isEquivalence = isEquivalence
        ; assoc = λ x y z → 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ˡ = λ x → iso [ ⊥-elim ∘ lower , id ]′ inj₂ (λ _ → refl) λ { (inj₁ abs) → ⊥-elim (lower abs); (inj₂ x) → refl }
      ; comm = λ x y → iso [ inj₂ , inj₁ ]′ [ inj₂ , inj₁ ]′ (λ { (inj₁ y) → refl ; (inj₂ x) → refl }) (λ { (inj₁ x) → refl ; (inj₂ y) → refl })
      }
    ; *-isCommutativeMonoid = record 
      { isSemigroup = record 
        { isEquivalence = isEquivalence
        ; assoc = λ x y z → iso (λ { ((x , y) , z) → x , y , z })
                                (λ { (x , y , z) → (x , y) , z })
                                (λ _ → refl)
                                (λ _ → refl)
        ; ∙-cong = ×-cong
        }
      ; identityˡ = λ x → iso proj₂ (_,_ (lift tt)) (λ _ → refl) (λ _ → refl)
      ; comm = λ x y → iso swap swap (λ _ → refl) (λ _ → refl)
      }
    ; distribʳ = λ x y z → iso (λ { (inj₁ y , x) → inj₁ (y , x); (inj₂ z , x) → inj₂ (z , x) })
                               (λ { (inj₁ (y , x)) → inj₁ y , x; (inj₂ (z , x)) → inj₂ z , x })
                               (λ { (inj₁ (y , x)) → refl; (inj₂ (z , x)) → refl })
                               (λ { (inj₁ y , x) → refl; (inj₂ z , x) → refl })
    ; zeroˡ = λ x → iso proj₁ (⊥-elim ∘ lower) (⊥-elim ∘ lower) (⊥-elim ∘ lower ∘ proj₁)
    }
  }

By Mr. Obvious