Skip to content

@copumpkin /Types.agda
Last active

Embed URL

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Types form a commutative semiring!
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₁)
}
}
@copumpkin
Owner

By Mr. Obvious

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Something went wrong with that request. Please try again.