This commit is contained in:
commit
75c95a0869
|
|
@ -0,0 +1,307 @@
|
|||
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 ∙₀)
|
||||
Loading…
Reference in New Issue