Last active
October 17, 2021 11:24
-
-
Save copumpkin/2636229 to your computer and use it in GitHub Desktop.
Types form a commutative semiring!
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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₁) | |
} | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
By Mr. Obvious