Instantly share code, notes, and snippets.

# copumpkin/Types.agda Last active Oct 4, 2015

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₁) } }
Owner

### copumpkin commented May 8, 2012

 By Mr. Obvious
to join this conversation on GitHub. Already have an account? Sign in to comment