public
Last active

Types form a commutative semiring!

  • Download Gist
Types.agda
Agda
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96
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₁)
}
}

Please sign in to comment on this gist.

Something went wrong with that request. Please try again.