From 66a0eac7e2c4d0733a7727e73036e776ddeb36e2 Mon Sep 17 00:00:00 2001 From: itamar Date: Fri, 10 Apr 2026 12:47:07 +0000 Subject: [PATCH] Delete main.agda --- main.agda | 297 ------------------------------------------------------ 1 file changed, 297 deletions(-) delete mode 100644 main.agda diff --git a/main.agda b/main.agda deleted file mode 100644 index cf134b0..0000000 --- a/main.agda +++ /dev/null @@ -1,297 +0,0 @@ -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 Σ - \ No newline at end of file