308 lines
12 KiB
Plaintext
308 lines
12 KiB
Plaintext
module Quotient.Algebra where
|
||
|
||
private
|
||
open import Relation.Binary.PropositionalEquality as P using (proof-irrelevance; _≡_)
|
||
open import Data.Nat using (ℕ; zero; suc)
|
||
|
||
open import Data.Vec.N-ary
|
||
|
||
N-ary-equality : ∀ {a} {A : Set a} (n : ℕ) → (f g : N-ary n A A) → Set (N-ary-level a a n)
|
||
N-ary-equality {A = A} n f g = Eq {A = A} n (_≡_ {A = A}) f g
|
||
|
||
private
|
||
module N-ary-equality-Ex where
|
||
open import Data.Nat
|
||
|
||
ex₀ : N-ary-equality {A = ℕ} 0 2 2
|
||
ex₀ = P.refl
|
||
|
||
ex₁ : N-ary-equality {A = ℕ} 1 suc (λ ξ → ξ + 1)
|
||
ex₁ zero = P.refl
|
||
ex₁ (suc n) = P.cong suc (ex₁ n)
|
||
|
||
open import Function using (flip)
|
||
|
||
ex₂ : N-ary-equality {A = ℕ} 2 _+_ (flip _+_)
|
||
ex₂ = +-comm
|
||
where
|
||
open import Algebra
|
||
import Data.Nat.Properties
|
||
open CommutativeSemiring Data.Nat.Properties.commutativeSemiring
|
||
|
||
N-ary-irrelevance : ∀ {a} {A : Set a} (n : ℕ) → Set (N-ary-level a a n)
|
||
N-ary-irrelevance {A = A} n = ∀ {f g} (p q : N-ary-equality {A = A} n f g) → p ≡ q
|
||
|
||
postulate
|
||
extensional-irrelevance : ∀ {a} {A : Set a} (n : ℕ) → N-ary-irrelevance {a} {A} n
|
||
|
||
private
|
||
module N-ary-irrelevance-Ex where
|
||
|
||
ex₀ : N-ary-irrelevance {A = ℕ} 0
|
||
ex₀ = proof-irrelevance
|
||
|
||
ex₁ : N-ary-irrelevance {A = ℕ} 1
|
||
ex₁ = extensional-irrelevance 1
|
||
|
||
open import Quotient
|
||
open import Algebra
|
||
open import Relation.Binary -- using (Setoid)
|
||
open import Algebra.Structures
|
||
|
||
open import Data.Product
|
||
open import Function
|
||
open import Algebra.FunctionProperties using (Op₁; Op₂)
|
||
|
||
import Algebra.FunctionProperties as FunProp
|
||
|
||
Sound₁ : ∀ {c ℓ} (S : Setoid c ℓ) → let open Setoid S in Op₁ Carrier → Set _
|
||
Sound₁ S f = let open Setoid S in f Preserves _≈_ ⟶ _≈_
|
||
|
||
quot₁ : ∀ {c ℓ} {S : Setoid c ℓ} → let open Setoid S in
|
||
{f : Op₁ Carrier} → (∙-sound : Sound₁ S f) → Op₁ (Quotient S)
|
||
quot₁ {S = S} {f} prf = rec _ (λ x → [ f x ]) (λ x≈x′ → [ prf x≈x′ ]-cong)
|
||
where
|
||
open Setoid S
|
||
|
||
Sound₂ : ∀ {c ℓ} (S : Setoid c ℓ) → let open Setoid S in Op₂ Carrier → Set _
|
||
Sound₂ S ∙ = let open Setoid S in ∙ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_
|
||
|
||
quot₂ : ∀ {c ℓ} {S : Setoid c ℓ} → let open Setoid S in
|
||
{∙ : Op₂ Carrier} → (∙-sound : Sound₂ S ∙) → Op₂ (Quotient S)
|
||
quot₂ {S = S} {_∙_} prf = rec S (λ x → rec _ (λ y → [ x ∙ y ])
|
||
(λ y≈y′ → [ refl ⟨ prf ⟩ y≈y′ ]-cong))
|
||
-- (λ {x} {x′} x≈x′ → P.cong (λ ξ → rec S ξ _)
|
||
-- (extensionality (λ _ → [ x≈x′ ⟨ prf ⟩ refl ]-cong)))
|
||
(λ x≈x′ → extensionality (elim _ _ (λ _ → [ (x≈x′ ⟨ prf ⟩ refl) ]-cong)
|
||
(λ _ → proof-irrelevance _ _)))
|
||
where
|
||
open Setoid S
|
||
postulate extensionality : P.Extensionality _ _
|
||
|
||
|
||
quot-assoc : ∀ {c ℓ} {S : Setoid c ℓ} →
|
||
let
|
||
open Setoid S
|
||
module F₀ = FunProp _≈_
|
||
module F = FunProp (_≡_ {A = Quotient S})
|
||
in
|
||
{∙ : Op₂ Carrier} → (∙-sound : Sound₂ S ∙) →
|
||
F₀.Associative ∙ → F.Associative (quot₂ ∙-sound)
|
||
quot-assoc {S = S} sound prf
|
||
= elim S _
|
||
(λ x → elim S _ (λ y → elim S _ (λ z → [ prf x y z ]-cong)
|
||
(λ _ → extensional-irrelevance 0 _ _))
|
||
(λ _ → extensional-irrelevance 1 _ _))
|
||
(λ _ → extensional-irrelevance 2 _ _)
|
||
|
||
quot-comm : ∀ {c ℓ} {S : Setoid c ℓ} →
|
||
let
|
||
open Setoid S
|
||
module F₀ = FunProp _≈_
|
||
module F = FunProp (_≡_ {A = Quotient S})
|
||
in
|
||
{∙ : Op₂ Carrier} → (∙-sound : Sound₂ S ∙) →
|
||
F₀.Commutative ∙ → F.Commutative (quot₂ ∙-sound)
|
||
quot-comm {S = S} sound prf
|
||
= elim S _ (λ x → elim S _ (λ y → [ prf x y ]-cong)
|
||
(λ _ → extensional-irrelevance 0 _ _))
|
||
(λ _ → extensional-irrelevance 1 _ _)
|
||
|
||
quot-leftDistrib : ∀ {c ℓ} {S : Setoid c ℓ} →
|
||
let
|
||
open Setoid S
|
||
module F₀ = FunProp _≈_
|
||
module F = FunProp (_≡_ {A = Quotient S})
|
||
in
|
||
{* : Op₂ Carrier} → (*-sound : Sound₂ S *) →
|
||
{+ : Op₂ Carrier} → (+-sound : Sound₂ S +) →
|
||
* F₀.DistributesOverˡ + →
|
||
(quot₂ *-sound) F.DistributesOverˡ (quot₂ +-sound)
|
||
quot-leftDistrib {S = S} {*} *-sound {+} +-sound prf
|
||
= elim S _ (λ x → elim S _ (λ y → elim S _ (λ z → [ prf x y z ]-cong)
|
||
(λ _ → extensional-irrelevance 0 _ _))
|
||
(λ _ → extensional-irrelevance 1 _ _))
|
||
(λ _ → extensional-irrelevance 2 _ _)
|
||
|
||
quot-rightDistrib : ∀ {c ℓ} {S : Setoid c ℓ} →
|
||
let
|
||
open Setoid S
|
||
module F₀ = FunProp _≈_
|
||
module F = FunProp (_≡_ {A = Quotient S})
|
||
in
|
||
{* : Op₂ Carrier} → (*-sound : Sound₂ S *) →
|
||
{+ : Op₂ Carrier} → (+-sound : Sound₂ S +) →
|
||
* F₀.DistributesOverʳ + →
|
||
(quot₂ *-sound) F.DistributesOverʳ (quot₂ +-sound)
|
||
quot-rightDistrib {S = S} {*} *-sound {+} +-sound prf
|
||
= elim S _ (λ x → elim S _ (λ y → elim S _ (λ z → [ prf x y z ]-cong)
|
||
(λ _ → extensional-irrelevance 0 _ _))
|
||
(λ _ → extensional-irrelevance 1 _ _))
|
||
(λ _ → extensional-irrelevance 2 _ _)
|
||
|
||
quot-distrib : ∀ {c ℓ} {S : Setoid c ℓ} →
|
||
let
|
||
open Setoid S
|
||
module F₀ = FunProp _≈_
|
||
module F = FunProp (_≡_ {A = Quotient S})
|
||
in
|
||
{* : Op₂ Carrier} → (*-sound : Sound₂ S *) →
|
||
{+ : Op₂ Carrier} → (+-sound : Sound₂ S +) →
|
||
* F₀.DistributesOver + →
|
||
(quot₂ *-sound) F.DistributesOver (quot₂ +-sound)
|
||
quot-distrib *-sound +-sound prf
|
||
= quot-leftDistrib *-sound +-sound (proj₁ prf) , quot-rightDistrib *-sound +-sound (proj₂ prf)
|
||
|
||
quot-leftIdentity : ∀ {c ℓ} {S : Setoid c ℓ} →
|
||
let
|
||
open Setoid S
|
||
module F₀ = FunProp _≈_
|
||
module F = FunProp (_≡_ {A = Quotient S})
|
||
in
|
||
{∙ : Op₂ Carrier} → (∙-sound : Sound₂ S ∙) →
|
||
{ε : Carrier} →
|
||
F₀.LeftIdentity ε ∙ → F.LeftIdentity [ ε ] (quot₂ ∙-sound)
|
||
quot-leftIdentity {S = S} {∙} sound {ε} prf
|
||
= elim S _ (λ x → [ prf x ]-cong)
|
||
(λ _ → extensional-irrelevance 0 _ _)
|
||
|
||
quot-rightIdentity : ∀ {c ℓ} {S : Setoid c ℓ} →
|
||
let
|
||
open Setoid S
|
||
module F₀ = FunProp _≈_
|
||
module F = FunProp (_≡_ {A = Quotient S})
|
||
in
|
||
{∙ : Op₂ Carrier} → (∙-sound : Sound₂ S ∙) →
|
||
{ε : Carrier} →
|
||
F₀.RightIdentity ε ∙ → F.RightIdentity [ ε ] (quot₂ ∙-sound)
|
||
quot-rightIdentity {S = S} {∙} sound {ε} prf
|
||
= elim S _
|
||
(λ x → [ prf x ]-cong)
|
||
(λ _ → extensional-irrelevance 0 _ _)
|
||
|
||
quot-identity : ∀ {c ℓ} {S : Setoid c ℓ} →
|
||
let
|
||
open Setoid S
|
||
module F₀ = FunProp _≈_
|
||
module F = FunProp (_≡_ {A = Quotient S})
|
||
in
|
||
{∙ : Op₂ Carrier} → (∙-sound : Sound₂ S ∙) →
|
||
{ε : Carrier} →
|
||
F₀.Identity ε ∙ → F.Identity [ ε ] (quot₂ ∙-sound)
|
||
quot-identity sound (prfˡ , prfʳ)
|
||
= quot-leftIdentity sound prfˡ , quot-rightIdentity sound prfʳ
|
||
|
||
quot-leftInverse : ∀ {c ℓ} {S : Setoid c ℓ} →
|
||
let
|
||
open Setoid S
|
||
module F₀ = FunProp _≈_
|
||
module F = FunProp (_≡_ {A = Quotient S})
|
||
in
|
||
{⁻¹ : Op₁ Carrier} → (⁻¹-sound : Sound₁ S ⁻¹) →
|
||
{∙ : Op₂ Carrier} → (∙-sound : Sound₂ S ∙) →
|
||
{ε : Carrier} →
|
||
F₀.LeftInverse ε ⁻¹ ∙ → F.LeftInverse [ ε ] (quot₁ ⁻¹-sound) (quot₂ ∙-sound)
|
||
quot-leftInverse {S = S} {_⁻¹} ⁻¹-sound {_∙_} ∙-sound {ε} prf
|
||
= elim S _
|
||
(λ x → [ prf x ]-cong)
|
||
(λ _ → extensional-irrelevance 0 _ _)
|
||
|
||
quot-rightInverse : ∀ {c ℓ} {S : Setoid c ℓ} →
|
||
let
|
||
open Setoid S
|
||
module F₀ = FunProp _≈_
|
||
module F = FunProp (_≡_ {A = Quotient S})
|
||
in
|
||
{⁻¹ : Op₁ Carrier} → (⁻¹-sound : Sound₁ S ⁻¹) →
|
||
{∙ : Op₂ Carrier} → (∙-sound : Sound₂ S ∙) →
|
||
{ε : Carrier} →
|
||
F₀.RightInverse ε ⁻¹ ∙ → F.RightInverse [ ε ] (quot₁ ⁻¹-sound) (quot₂ ∙-sound)
|
||
quot-rightInverse {S = S} {_⁻¹} ⁻¹-sound {_∙_} ∙-sound {ε} prf
|
||
= elim S _
|
||
(λ x → [ prf x ]-cong)
|
||
(λ _ → extensional-irrelevance 0 _ _)
|
||
|
||
quot-inverse : ∀ {c ℓ} {S : Setoid c ℓ} →
|
||
let
|
||
open Setoid S
|
||
module F₀ = FunProp _≈_
|
||
module F = FunProp (_≡_ {A = Quotient S})
|
||
in
|
||
{⁻¹ : Op₁ Carrier} → (⁻¹-sound : Sound₁ S ⁻¹) →
|
||
{∙ : Op₂ Carrier} → (∙-sound : Sound₂ S ∙) →
|
||
{ε : Carrier} →
|
||
F₀.Inverse ε ⁻¹ ∙ → F.Inverse [ ε ] (quot₁ ⁻¹-sound) (quot₂ ∙-sound)
|
||
quot-inverse ⁻¹-sound ∙-sound (prfˡ , prfʳ)
|
||
= quot-leftInverse ⁻¹-sound ∙-sound prfˡ , quot-rightInverse ⁻¹-sound ∙-sound prfʳ
|
||
|
||
quot-isSemigroup : ∀ {c ℓ} → (Σ : Semigroup c ℓ) → let open Semigroup Σ in
|
||
IsSemigroup (_≡_ {A = Quotient setoid}) (quot₂ ∙-cong)
|
||
quot-isSemigroup Σ = record
|
||
{ isEquivalence = Relation.Binary.Setoid.isEquivalence (P.setoid _)
|
||
; assoc = quot-assoc ∙-cong assoc
|
||
; ∙-cong = P.cong₂ _
|
||
}
|
||
where
|
||
open Semigroup Σ
|
||
|
||
quot-isMonoid : ∀ {c ℓ} → (Σ : Monoid c ℓ) → let open Monoid Σ in
|
||
IsMonoid (_≡_ {A = Quotient setoid}) (quot₂ ∙-cong) [ ε ]
|
||
quot-isMonoid Σ = record
|
||
{ isSemigroup = quot-isSemigroup semigroup
|
||
; identity = quot-identity ∙-cong identity
|
||
}
|
||
where
|
||
open Monoid Σ
|
||
|
||
quot-isGroup : ∀ {c ℓ} → (Σ : Group c ℓ) → let open Group Σ in
|
||
IsGroup (_≡_ {A = Quotient setoid}) (quot₂ ∙-cong) [ ε ] (quot₁ ⁻¹-cong)
|
||
quot-isGroup Σ = record
|
||
{ isMonoid = quot-isMonoid monoid
|
||
; inverse = quot-inverse ⁻¹-cong ∙-cong inverse
|
||
; ⁻¹-cong = P.cong _
|
||
}
|
||
where
|
||
open Group Σ
|
||
|
||
quot-isAbelianGroup : ∀ {c ℓ} → (Σ : AbelianGroup c ℓ) → let open AbelianGroup Σ in
|
||
IsAbelianGroup (_≡_ {A = Quotient setoid}) (quot₂ ∙-cong) [ ε ] (quot₁ ⁻¹-cong)
|
||
quot-isAbelianGroup Σ = record
|
||
{ isGroup = quot-isGroup group
|
||
; comm = quot-comm ∙-cong comm
|
||
}
|
||
where
|
||
open AbelianGroup Σ
|
||
|
||
quot-isRing : ∀ {c ℓ} → (Σ : Ring c ℓ) → let open Ring Σ in
|
||
IsRing (_≡_ {A = Quotient setoid}) (quot₂ +-cong) (quot₂ *-cong) (quot₁ -‿cong) [ 0# ] [ 1# ]
|
||
quot-isRing Σ = record
|
||
{ +-isAbelianGroup = quot-isAbelianGroup +-abelianGroup
|
||
; *-isMonoid = quot-isMonoid (record
|
||
{ Carrier = Carrier
|
||
; _≈_ = _≈_
|
||
; _∙_ = _*_
|
||
; ε = 1#
|
||
; isMonoid = record
|
||
{ isSemigroup = record
|
||
{ isEquivalence = isEquivalence
|
||
; assoc = *-assoc
|
||
; ∙-cong = *-cong
|
||
}
|
||
; identity = *-identity }
|
||
})
|
||
; distrib = quot-distrib *-cong +-cong distrib
|
||
}
|
||
where
|
||
open Ring Σ
|
||
|
||
-- quot-semigroup : ∀ {c ℓ} → (Σ : Semigroup c ℓ) →
|
||
-- Semigroup (ℓ ⊔ c) (ℓ ⊔ c)
|
||
-- quot-semigroup Σ = record
|
||
-- { Carrier = Quotient setoid
|
||
-- ; _≈_ = _≡_
|
||
-- ; _∙_ = quot₂ ∙₀ ∙-cong
|
||
-- ; isSemigroup = quot-isSemigroup Σ
|
||
-- }
|
||
-- where
|
||
-- open Semigroup Σ renaming (_∙_ to ∙₀)
|