------------------------------------------------------------------------
-- The Agda standard library
--
-- Algebraic properties of sums (disjoint unions)
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Sum.Algebra where
open import Algebra.Bundles
using (Magma; Semigroup; Monoid; CommutativeMonoid)
open import Algebra.Definitions
using (Associative; LeftIdentity; RightIdentity; Identity)
open import Algebra.Structures
using (IsMagma; IsSemigroup; IsMonoid; IsCommutativeMonoid)
open import Data.Empty.Polymorphic using (⊥)
open import Data.Product.Base using (_,_)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂; map; [_,_]; swap; assocʳ; assocˡ)
open import Data.Sum.Properties using (swap-involutive)
open import Data.Unit.Polymorphic.Base using (⊤; tt)
open import Function.Base using (id; _∘_)
open import Function.Properties.Inverse using (↔-isEquivalence)
open import Function.Bundles using (_↔_; Inverse; mk↔ₛ′)
open import Level using (Level; suc)
open import Relation.Binary.PropositionalEquality.Core
using (_≡_; refl; cong; cong′)
import Function.Definitions as FuncDef
------------------------------------------------------------------------
-- Setup
private
variable
a b c d : Level
A B C D : Set a
♯ : {B : ⊥ {a} → Set b} → (w : ⊥) → B w
♯ ()
------------------------------------------------------------------------
-- Algebraic properties
⊎-cong : A ↔ B → C ↔ D → (A ⊎ C) ↔ (B ⊎ D)
⊎-cong i j = mk↔ₛ′ (map I.to J.to) (map I.from J.from)
[ cong inj₁ ∘ I.strictlyInverseˡ , cong inj₂ ∘ J.strictlyInverseˡ ]
[ cong inj₁ ∘ I.strictlyInverseʳ , cong inj₂ ∘ J.strictlyInverseʳ ]
where module I = Inverse i; module J = Inverse j
-- ⊎ is commutative.
-- We don't use Commutative because it isn't polymorphic enough.
⊎-comm : (A : Set a) (B : Set b) → (A ⊎ B) ↔ (B ⊎ A)
⊎-comm _ _ = mk↔ₛ′ swap swap swap-involutive swap-involutive
module _ (ℓ : Level) where
-- ⊎ is associative
⊎-assoc : Associative {ℓ = ℓ} _↔_ _⊎_
⊎-assoc _ _ _ = mk↔ₛ′ assocʳ assocˡ
[ cong′ , [ cong′ , cong′ ] ] [ [ cong′ , cong′ ] , cong′ ]
-- ⊥ is an identity for ⊎
⊎-identityˡ : LeftIdentity {ℓ = ℓ} _↔_ ⊥ _⊎_
⊎-identityˡ A = mk↔ₛ′ [ ♯ , id ] inj₂ cong′ [ ♯ , cong′ ]
⊎-identityʳ : RightIdentity {ℓ = ℓ} _↔_ ⊥ _⊎_
⊎-identityʳ _ = mk↔ₛ′ [ id , ♯ ] inj₁ cong′ [ cong′ , ♯ ]
⊎-identity : Identity _↔_ ⊥ _⊎_
⊎-identity = ⊎-identityˡ , ⊎-identityʳ
------------------------------------------------------------------------
-- Algebraic structures
⊎-isMagma : IsMagma {ℓ = ℓ} _↔_ _⊎_
⊎-isMagma = record
{ isEquivalence = ↔-isEquivalence
; ∙-cong = ⊎-cong
}
⊎-isSemigroup : IsSemigroup _↔_ _⊎_
⊎-isSemigroup = record
{ isMagma = ⊎-isMagma
; assoc = ⊎-assoc
}
⊎-isMonoid : IsMonoid _↔_ _⊎_ ⊥
⊎-isMonoid = record
{ isSemigroup = ⊎-isSemigroup
; identity = ⊎-identityˡ , ⊎-identityʳ
}
⊎-isCommutativeMonoid : IsCommutativeMonoid _↔_ _⊎_ ⊥
⊎-isCommutativeMonoid = record
{ isMonoid = ⊎-isMonoid
; comm = ⊎-comm
}
------------------------------------------------------------------------
-- Algebraic bundles
⊎-magma : Magma (suc ℓ) ℓ
⊎-magma = record
{ isMagma = ⊎-isMagma
}
⊎-semigroup : Semigroup (suc ℓ) ℓ
⊎-semigroup = record
{ isSemigroup = ⊎-isSemigroup
}
⊎-monoid : Monoid (suc ℓ) ℓ
⊎-monoid = record
{ isMonoid = ⊎-isMonoid
}
⊎-commutativeMonoid : CommutativeMonoid (suc ℓ) ℓ
⊎-commutativeMonoid = record
{ isCommutativeMonoid = ⊎-isCommutativeMonoid
}
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4