Merge branch 'main' into joint-monos

src/1Lab/Reflection/Induction/Examples.agda

@@ -12,14 +12,6 @@ open import Homotopy.Space.Circle hiding (S¹-elim)
 
 module 1Lab.Reflection.Induction.Examples where
 
-unquoteDecl Fin-elim = make-elim Fin-elim (quote Fin)
-
-_ : {ℓ : Level} {P : {n : Nat} (f : Fin n) → Type ℓ}
-    (P0 : {n : Nat} → P fzero)
-    (Psuc : {n : Nat} (f : Fin n) (Pf : P f) → P (fsuc f))
-    {n : Nat} (f : Fin n) → P f
-_ = Fin-elim
-
 unquoteDecl J = make-elim-with default-elim-visible J (quote _≡ᵢ_)
 
 _ : {ℓ : Level} {A : Type ℓ} {x : A} {ℓ₁ : Level}

src/1Lab/Reflection/Variables.agda

@@ -66,9 +66,12 @@ private
   ... | nothing      | yes _ = just tm-var
   ... | nothing      | no _  = nothing
 
+  fzero' : ∀ {n} → Fin (suc n)
+  fzero' = fzero
+
   fin-term : Nat → Term
-  fin-term zero = con (quote fzero) (unknown h∷ [])
-  fin-term (suc n) = con (quote fsuc) (unknown h∷ fin-term n v∷ [])
+  fin-term zero    = def (quote fzero') (unknown h∷ [])
+  fin-term (suc n) = def (quote fsuc)   (unknown h∷ fin-term n v∷ [])
 
   env-rec : (Mot : Nat → Type b) →
           (∀ {n} → Mot n → A → Mot (suc n)) →

src/1Lab/Type.lagda.md

@@ -138,5 +138,8 @@ instance
   Number-Lift : ∀ {ℓ ℓ'} {A : Type ℓ} → ⦃ Number A ⦄ → Number (Lift ℓ' A)
   Number-Lift {ℓ' = ℓ'} ⦃ a ⦄ .Number.Constraint n = Lift ℓ' (a .Number.Constraint n)
   Number-Lift ⦃ a ⦄ .Number.fromNat n ⦃ lift c ⦄ = lift (a .Number.fromNat n ⦃ c ⦄)
+
+absurdω : {A : Typeω} → .⊥ → A
+absurdω ()
 ```
 -->

src/Algebra/Group.lagda.md

@@ -271,8 +271,8 @@ record make-group {ℓ} (G : Type ℓ) : Type ℓ where
     idl   : ∀ x → mul unit x ≡ x
 
   private
-    inverser : ∀ x → mul x (inv x) ≡ unit
-    inverser x =
+    invr : ∀ x → mul x (inv x) ≡ unit
+    invr x =
       mul x (inv x)                                   ≡˘⟨ idl _ ⟩
       mul unit (mul x (inv x))                        ≡˘⟨ ap₂ mul (invl _) refl ⟩
       mul (mul (inv (inv x)) (inv x)) (mul x (inv x)) ≡˘⟨ assoc _ _ _ ⟩
@@ -282,23 +282,26 @@ record make-group {ℓ} (G : Type ℓ) : Type ℓ where
       mul (inv (inv x)) (inv x)                       ≡⟨ invl _ ⟩
       unit                                            ∎
 
-  to-group-on : Group-on G
-  to-group-on .Group-on._⋆_ = mul
-  to-group-on .Group-on.has-is-group .is-group.unit = unit
-  to-group-on .Group-on.has-is-group .is-group.inverse = inv
-  to-group-on .Group-on.has-is-group .is-group.inversel = invl _
-  to-group-on .Group-on.has-is-group .is-group.inverser = inverser _
-  to-group-on .Group-on.has-is-group .is-group.has-is-monoid .is-monoid.idl {x} = idl x
-  to-group-on .Group-on.has-is-group .is-group.has-is-monoid .is-monoid.idr {x} =
+  to-is-group : is-group mul
+  to-is-group .is-group.unit = unit
+  to-is-group .is-group.inverse = inv
+  to-is-group .is-group.inversel = invl _
+  to-is-group .is-group.inverser = invr _
+  to-is-group .is-group.has-is-monoid .is-monoid.idl {x} = idl x
+  to-is-group .is-group.has-is-monoid .is-monoid.idr {x} =
     mul x ⌜ unit ⌝           ≡˘⟨ ap¡ (invl x) ⟩
     mul x (mul (inv x) x)    ≡⟨ assoc _ _ _ ⟩
-    mul ⌜ mul x (inv x) ⌝ x  ≡⟨ ap! (inverser x) ⟩
+    mul ⌜ mul x (inv x) ⌝ x  ≡⟨ ap! (invr x) ⟩
     mul unit x               ≡⟨ idl x ⟩
     x                        ∎
-  to-group-on .Group-on.has-is-group .is-group.has-is-monoid .has-is-semigroup =
+  to-is-group .is-group.has-is-monoid .has-is-semigroup =
     record { has-is-magma = record { has-is-set = group-is-set }
            ; associative = λ {x y z} → assoc x y z
            }
 
-open make-group using (to-group-on) public
+  to-group-on : Group-on G
+  to-group-on .Group-on._⋆_ = mul
+  to-group-on .Group-on.has-is-group = to-is-group
+
+open make-group using (to-is-group; to-group-on) public
 ```

src/Algebra/Group/Ab.lagda.md

@@ -153,15 +153,18 @@ record make-abelian-group (T : Type ℓ) : Type ℓ where
     mg .make-group.invl   = invl
     mg .make-group.idl    = idl
 
+  to-is-abelian-group : is-abelian-group mul
+  to-is-abelian-group .is-abelian-group.has-is-group =
+    to-is-group make-abelian-group→make-group
+  to-is-abelian-group .is-abelian-group.commutes =
+    comm _ _
+
   to-group-on-ab : Group-on T
   to-group-on-ab = to-group-on make-abelian-group→make-group
 
   to-abelian-group-on : Abelian-group-on T
   to-abelian-group-on .Abelian-group-on._*_ = mul
-  to-abelian-group-on .Abelian-group-on.has-is-ab .is-abelian-group.has-is-group =
-    Group-on.has-is-group to-group-on-ab
-  to-abelian-group-on .Abelian-group-on.has-is-ab .is-abelian-group.commutes =
-    comm _ _
+  to-abelian-group-on .Abelian-group-on.has-is-ab = to-is-abelian-group
 
   to-ab : Abelian-group ℓ
   ∣ to-ab .fst ∣ = T
@@ -191,7 +194,7 @@ Grp→Ab→Grp G c = Σ-pathp refl go where
   go i .Group-on._⋆_ = G .snd .Group-on._⋆_
   go i .Group-on.has-is-group = G .snd .Group-on.has-is-group
 
-open make-abelian-group using (make-abelian-group→make-group ; to-group-on-ab ; to-abelian-group-on ; to-ab) public
+open make-abelian-group using (make-abelian-group→make-group ; to-group-on-ab ; to-is-abelian-group ; to-abelian-group-on ; to-ab) public
 
 open Functor
 

src/Algebra/Group/Instances/Cyclic.lagda.md

@@ -12,9 +12,11 @@ open import Cat.Prelude
 open import Data.Int.Divisible
 open import Data.Int.Universal
 open import Data.Fin.Closure
+open import Data.Fin.Product
 open import Data.Int.DivMod
 open import Data.Fin
 open import Data.Int hiding (Positive)
+open import Data.Irr
 open import Data.Nat
 
 open represents-subgroup
@@ -182,17 +184,14 @@ $x : \ZZ$ to the representative of its congruence class modulo $n$,
 $x \% n$.
 
 ```agda
-ℤ/n≃ℕ<n : ∀ n → .⦃ Positive n ⦄ → ⌞ ℤ/ n ⌟ ≃ ℕ< n
-ℤ/n≃ℕ<n n .fst = Coeq-rec (λ i → i %ℤ n , x%ℤy<y i n)
-  λ (x , y , p) → Σ-prop-path! (divides-diff→same-rem n x y p)
-ℤ/n≃ℕ<n n .snd = is-iso→is-equiv $ iso
-  (λ (i , p) → inc (pos i))
-  (λ i → Σ-prop-path! (ℕ<-%ℤ i))
-  (elim! λ i → quot (same-rem→divides-diff n (pos (i %ℤ n)) i
-    (ℕ<-%ℤ (_ , x%ℤy<y i n))))
-
 Finite-ℤ/n : ∀ n → .⦃ Positive n ⦄ → ⌞ ℤ/ n ⌟ ≃ Fin n
-Finite-ℤ/n n = ℤ/n≃ℕ<n n ∙e Fin≃ℕ< e⁻¹
+Finite-ℤ/n n .fst = Coeq-rec (λ i → from-ℕ< (i %ℤ n , x%ℤy<y i n))
+  λ (x , y , p) → fin-ap (divides-diff→same-rem n x y p)
+Finite-ℤ/n n .snd = is-iso→is-equiv $ iso
+  (λ (fin i) → inc (pos i))
+  (λ i → fin-ap (Fin-%ℤ i))
+  (elim! λ i → quot (same-rem→divides-diff n (pos (i %ℤ n)) i
+    (Fin-%ℤ (fin _ ⦃ forget (x%ℤy<y i n) ⦄))))
 ```
 
 Using this and the fact that $([2] \simeq [2]) \simeq [2!] = [2]$,
@@ -229,8 +228,6 @@ equivalences:
 ℤ/2≡S₂ = ∫-Path ℤ/2→S₂ $
   equiv-cancell (Fin-permutations 2 .snd)
     (equiv-cancelr ((Finite-ℤ/n 2 e⁻¹) .snd)
-      (subst is-equiv (ext λ where
-        fzero → refl
-        (fsuc fzero) → refl)
+      (subst is-equiv (ext (indexₚ (refl , refl , tt)))
       id-equiv))
 ```

src/Algebra/Group/NAry.lagda.md

@@ -77,10 +77,11 @@ module _ {ℓ} {T : Type ℓ} (G : Group-on T)  where
     → f i ≡ x
     → (∀ j → ¬ i ≡ j → f j ≡ G.unit)
     → ∑ G f ≡ x
-  ∑-diagonal-lemma {suc n} fzero f f0=x fj=0 =
+  ∑-diagonal-lemma i _ _ _ with fin-view i
+  ∑-diagonal-lemma {suc n} _ f f0=x fj=0 | zero =
     G.elimr ( ∑-path {n = n} G (λ i → fj=0 (fsuc i) fzero≠fsuc)
             ∙ ∑-zero {n = n} G) ∙ f0=x
-  ∑-diagonal-lemma {suc n} (fsuc i) {x} f fj=x f≠i=0 =
+  ∑-diagonal-lemma {suc n} _ {x} f fj=x f≠i=0 | suc i =
     f fzero G.⋆ ∑ {n} G (λ e → f (fsuc e)) ≡⟨ G.eliml (f≠i=0 fzero λ e → fzero≠fsuc (sym e)) ⟩
     ∑ {n} G (λ e → f (fsuc e))             ≡⟨ ∑-diagonal-lemma {n} i (λ e → f (fsuc e)) fj=x (λ j i≠j → f≠i=0 (fsuc j) (λ e → i≠j (fsuc-inj e))) ⟩
     x                                      ∎

src/Algebra/Magma.lagda.md

@@ -68,7 +68,7 @@ binary operation `⋆`, on which no further laws are imposed.
     magma-hlevel : ∀ {n} → H-Level A (2 + n)
     magma-hlevel = basic-instance 2 has-is-set
 
-open is-magma public
+open is-magma
 ```
 
 Note that we do not generally benefit from the [[set truncation]] of
@@ -84,6 +84,16 @@ is-magma-is-prop x y i .has-is-set =
   is-hlevel-is-prop 2 (x .has-is-set) (y .has-is-set) i
 ```
 
+<!--
+```agda
+instance
+  H-Level-is-magma
+    : ∀ {ℓ} {A : Type ℓ} {_⋆_ : A → A → A} {n}
+    → H-Level (is-magma _⋆_) (suc n)
+  H-Level-is-magma = prop-instance is-magma-is-prop
+```
+-->
+
 By turning the operation parameter into an additional piece of data, we
 get the notion of a **magma structure** on a type, as well as the
 notion of a magma in general by doing the same to the carrier type.

src/Algebra/Magma/Unital/EckmannHilton.lagda.md

@@ -102,8 +102,8 @@ unitality allows us to prove that the operation is a monoid.
     x ⋆ (y ⋆ z) ∎)
 
   ⋆-is-monoid : is-monoid e _⋆_
-  ⋆-is-monoid .has-is-semigroup .has-is-magma = unital-mgm .has-is-magma
-  ⋆-is-monoid .has-is-semigroup .associative = ⋆-associative _ _ _
+  ⋆-is-monoid .has-is-semigroup .is-semigroup.has-is-magma = unital-mgm .has-is-magma
+  ⋆-is-monoid .has-is-semigroup .is-semigroup.associative = ⋆-associative _ _ _
   ⋆-is-monoid .idl = unital-mgm .idl
   ⋆-is-monoid .idr = unital-mgm .idr
 ```

src/Algebra/Monoid.lagda.md

@@ -80,8 +80,6 @@ record Monoid-on (A : Type ℓ) : Type ℓ where
 
 Monoid : (ℓ : Level) → Type (lsuc ℓ)
 Monoid ℓ = Σ (Type ℓ) Monoid-on
-
-open Monoid-on
 ```
 
 There is also a predicate which witnesses when an equivalence between
@@ -125,7 +123,7 @@ First, we show that every monoid is a unital magma:
 ```agda
 module _ {id : A} {_⋆_ : A → A → A} where
   is-monoid→is-unital-magma : is-monoid id _⋆_ → is-unital-magma id _⋆_
-  is-monoid→is-unital-magma mon .has-is-magma = mon .has-is-semigroup .has-is-magma
+  is-monoid→is-unital-magma mon .has-is-magma = mon .has-is-magma
   is-monoid→is-unital-magma mon .idl = mon .idl
   is-monoid→is-unital-magma mon .idr = mon .idr
 ```
@@ -172,3 +170,33 @@ monoid-inverse-unique {1M = 1M} {_⋆_} m e x y li1 ri2 =
   1M ⋆ y        ≡⟨ m .idl ⟩
   y             ∎
 ```
+
+# Constructing monoids
+
+The interface to `Monoid-on`{.Agda} is contains some annoying nesting,
+so we provide an interface that arranges the data in a more user-friendly
+way.
+
+```agda
+record make-monoid {ℓ} (A : Type ℓ) : Type ℓ where
+  field
+    monoid-is-set : is-set A
+    _⋆_ : A → A → A
+    1M : A
+    ⋆-assoc : ∀ x y z → x ⋆ (y ⋆ z) ≡ (x ⋆ y) ⋆ z
+    ⋆-idl : ∀ x → 1M ⋆ x ≡ x
+    ⋆-idr : ∀ x → x ⋆ 1M ≡ x
+
+  to-is-monoid : is-monoid 1M _⋆_
+  to-is-monoid .has-is-semigroup .is-semigroup.has-is-magma = record { has-is-set = monoid-is-set }
+  to-is-monoid .has-is-semigroup .is-semigroup.associative = ⋆-assoc _ _ _
+  to-is-monoid .idl = ⋆-idl _
+  to-is-monoid .idr = ⋆-idr _
+
+  to-monoid-on : Monoid-on A
+  to-monoid-on .Monoid-on.identity = 1M
+  to-monoid-on .Monoid-on._⋆_ = _⋆_
+  to-monoid-on .Monoid-on.has-is-monoid = to-is-monoid
+
+open make-monoid using (to-is-monoid; to-monoid-on) public
+```