commit 75c95a086912d8409f4d67bada703de1c0f7847a
Author: cat <zkdream@protonmail.com>
Date:   Mon Mar 11 20:22:08 2024 +0200

    P

diff --git a/main.agda b/main.agda
new file mode 100644
index 0000000..d7892d0
--- /dev/null
+++ b/main.agda
@@ -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 ∙₀)