From 7dbe6de0fd60a8119241262a9f0a7270e9de2530 Mon Sep 17 00:00:00 2001 From: Garrett Figueroa Date: Sat, 15 Feb 2025 17:20:13 -0700 Subject: [PATCH] workinonit --- src/group-theory/left-quasigroups.lagda.md | 8 ++++++-- src/group-theory/right-quasigroups.lagda.md | 8 ++++++-- 2 files changed, 12 insertions(+), 4 deletions(-) diff --git a/src/group-theory/left-quasigroups.lagda.md b/src/group-theory/left-quasigroups.lagda.md index d2f97cdc97..2db67f4884 100644 --- a/src/group-theory/left-quasigroups.lagda.md +++ b/src/group-theory/left-quasigroups.lagda.md @@ -58,9 +58,13 @@ module _ is-prop-is-left-Quasigroup : is-prop is-left-Quasigroup is-prop-is-left-Quasigroup = - is-prop-Σ is-prop-is-left-cancellative-left-div (λ _ → is-prop-is-right-cancellative-left-div) + is-prop-Σ is-prop-is-left-cancellative-left-div + ( λ _ → is-prop-is-right-cancellative-left-div) left-Quasigroup : (l : Level) → UU (lsuc l) left-Quasigroup l = - Σ (Set l) (λ Q → Σ (type-Set Q → type-Set Q → type-Set Q) (λ mul → Σ (type-Set Q → type-Set Q → type-Set Q) λ left-div → is-left-Quasigroup Q mul left-div)) + Σ ( Set l) + ( λ Q → Σ (type-Set Q → type-Set Q → type-Set Q) + ( λ mul → Σ (type-Set Q → type-Set Q → type-Set Q) + ( λ left-div → is-left-Quasigroup Q mul left-div))) ``` diff --git a/src/group-theory/right-quasigroups.lagda.md b/src/group-theory/right-quasigroups.lagda.md index e6411d929f..06d880c3bb 100644 --- a/src/group-theory/right-quasigroups.lagda.md +++ b/src/group-theory/right-quasigroups.lagda.md @@ -60,9 +60,13 @@ module _ is-prop-is-right-Quasigroup : is-prop is-right-Quasigroup is-prop-is-right-Quasigroup = - is-prop-Σ is-prop-is-left-cancellative-right-div (λ _ → is-prop-is-right-cancellative-right-div) + is-prop-Σ is-prop-is-left-cancellative-right-div + ( λ _ → is-prop-is-right-cancellative-right-div) right-Quasigroup : (l : Level) → UU (lsuc l) right-Quasigroup l = - Σ (Set l) (λ Q → Σ (type-Set Q → type-Set Q → type-Set Q) (λ mul → Σ (type-Set Q → type-Set Q → type-Set Q) λ right-div → is-right-Quasigroup Q mul right-div)) + Σ ( Set l) + ( λ Q → Σ (type-Set Q → type-Set Q → type-Set Q) + ( λ mul → Σ (type-Set Q → type-Set Q → type-Set Q) + ( λ right-div → is-right-Quasigroup Q mul right-div))) ```