Merge branch 'master' into equality-iterated-sum-types

CITATION.cff

@@ -5,7 +5,7 @@ abstract: "The agda-unimath library is a community formalization project for uni
 authors:
   - family-names: "Rijke"
     given-names: "Egbert"
-  - family-names: "Bonnevier"
+  - family-names: "Stenholm"
     given-names: "Elisabeth"
   - family-names: "Prieto-Cubides"
     given-names: "Jonathan"

CITE-THIS-LIBRARY.md

@@ -5,7 +5,7 @@ BibTeX entry:
 
 ```text
 @software{agda-unimath,
-author = {Rijke, Egbert and Bonnevier, Elisabeth and Prieto-Cubides, Jonathan and Bakke, Fredrik and {others}},
+author = {Rijke, Egbert and Stenholm, Elisabeth and Prieto-Cubides, Jonathan and Bakke, Fredrik and {others}},
 license = {MIT},
 title = {{The agda-unimath library}},
 url = {https://github.com/UniMath/agda-unimath/}

CONTRIBUTORS.toml

@@ -32,11 +32,11 @@ in Trondheim. His research is on homotopy theory and higher category theory.
 '''
 
 [[contributors]]
-displayName = "Elisabeth Bonnevier"
+displayName = "Elisabeth Stenholm"
 maintainer = true
-usernames = [ "Elisabeth Bonnevier" ]
+usernames = [ "Elisabeth Stenholm", "Elisabeth Bonnevier" ]
 homepage = "https://elisabeth.bonnevier.one"
-github = "elisabethbonnevier"
+github = "elisabethstenholm"
 bio = '''
 Elisabeth is a PhD student at the University of Bergen. Her research is on
 homotopy type theory.

HOME.md

@@ -8,7 +8,7 @@ typed programming language [Agda](https://github.com/agda/agda).
 <img class="invertible-image" align="right" width="300" alt="agda-unimath" src="website/images/agda-unimath-logo.svg" />
 </a>
 
-The library project was created by Elisabeth Bonnevier, Jonathan Prieto-Cubides,
+The library project was created by Elisabeth Stenholm, Jonathan Prieto-Cubides,
 and Egbert Rijke, and is also maintained by Fredrik Bakke. Our goal is to create
 an online encyclopedia of formalized mathematics containing an extensive
 curriculum of topics from a univalent point of view. We think libraries of

README.md

@@ -2,8 +2,8 @@
 
 The `agda-unimath` library is a community formalization project for univalent
 mathematics in [Agda](https://github.com/agda/agda). The library project was
-created by Elisabeth Bonnevier, Jonathan Prieto-Cubides, and Egbert Rijke, and
-is also being maintained by Fredrik Bakke. Our goal is to formalize an extensive
+created by Elisabeth Stenholm, Jonathan Prieto-Cubides, and Egbert Rijke, and is
+also being maintained by Fredrik Bakke. Our goal is to formalize an extensive
 curriculum of mathematics from the univalent point of view. Furthermore, we
 think libraries of formalized mathematics have the potential to be useful, and
 informative resources for mathematicians. Our library is designed to work

src/category-theory/groupoids.lagda.md

@@ -76,8 +76,8 @@ module _
   id-hom-Groupoid = id-hom-Category category-Groupoid
 
   comp-hom-Groupoid :
-    {x y z : obj-Groupoid} → hom-Groupoid y z →
-    hom-Groupoid x y → hom-Groupoid x z
+    {x y z : obj-Groupoid} →
+    hom-Groupoid y z → hom-Groupoid x y → hom-Groupoid x z
   comp-hom-Groupoid = comp-hom-Category category-Groupoid
 
   associative-comp-hom-Groupoid :
@@ -136,30 +136,29 @@ module _
     fundamental-theorem-id
       ( is-contr-equiv'
         ( Σ ( Σ (type-1-Type X) (λ y → x ＝ y))
-            ( λ yp →
-              Σ ( Σ (pr1 yp ＝ x) (λ q → (q ∙ pr2 yp) ＝ refl))
-                ( λ ql → (pr2 yp ∙ pr1 ql) ＝ refl)))
+            ( λ (y , p) →
+              Σ ( Σ (y ＝ x) (λ q → q ∙ p ＝ refl))
+                ( λ (q , l) → p ∙ q ＝ refl)))
         ( ( equiv-tot
             ( λ y →
               equiv-tot
                 ( λ p →
                   associative-Σ
                     ( y ＝ x)
-                    ( λ q → (q ∙ p) ＝ refl)
-                    ( λ qr → (p ∙ pr1 qr) ＝ refl)))) ∘e
+                    ( λ q → q ∙ p ＝ refl)
+                    ( λ (q , r) → p ∙ q ＝ refl)))) ∘e
           ( associative-Σ
             ( type-1-Type X)
             ( λ y → x ＝ y)
-            ( λ yp →
-              Σ ( Σ (pr1 yp ＝ x) (λ q → (q ∙ pr2 yp) ＝ refl))
-                ( λ ql → (pr2 yp ∙ pr1 ql) ＝ refl))))
+            ( λ (y , p) →
+              Σ ( Σ (y ＝ x) (λ q → q ∙ p ＝ refl))
+                ( λ (q , l) → p ∙ q ＝ refl))))
         ( is-contr-iterated-Σ 2
           ( is-torsorial-path x ,
             ( x , refl) ,
             ( is-contr-equiv
               ( Σ (x ＝ x) (λ q → q ＝ refl))
-              ( equiv-tot
-                ( λ q → equiv-concat (inv right-unit) refl))
+              ( equiv-tot (λ q → equiv-concat (inv right-unit) refl))
               ( is-torsorial-path' refl)) ,
             ( refl , refl) ,
             ( is-proof-irrelevant-is-prop

src/finite-group-theory/cartier-delooping-sign-homomorphism.lagda.md

@@ -146,28 +146,28 @@ module _
       ( comp-hom-Group
         ( symmetric-Group (raise-Fin-Set l (n +ℕ 2)))
         ( loop-group-Set (raise-Fin-Set l (n +ℕ 2)))
-        ( abstract-group-Concrete-Group (UU-Fin-Group (lsuc l) 2))
+        ( group-Concrete-Group (UU-Fin-Group (lsuc l) 2))
         ( comp-hom-Group
           ( loop-group-Set (raise-Fin-Set l (n +ℕ 2)))
-          ( abstract-group-Concrete-Group (UU-Fin-Group l (n +ℕ 2)))
-          ( abstract-group-Concrete-Group (UU-Fin-Group (lsuc l) 2))
+          ( group-Concrete-Group (UU-Fin-Group l (n +ℕ 2)))
+          ( group-Concrete-Group (UU-Fin-Group (lsuc l) 2))
           ( hom-group-hom-Concrete-Group
             ( UU-Fin-Group l (n +ℕ 2))
             ( UU-Fin-Group (lsuc l) 2)
             ( cartier-delooping-sign (n +ℕ 2)))
           ( hom-inv-iso-Group
-            ( abstract-group-Concrete-Group (UU-Fin-Group l (n +ℕ 2)))
+            ( group-Concrete-Group (UU-Fin-Group l (n +ℕ 2)))
             ( loop-group-Set (raise-Fin-Set l (n +ℕ 2)))
             ( iso-loop-group-fin-UU-Fin-Group l (n +ℕ 2))))
         ( hom-inv-symmetric-group-loop-group-Set (raise-Fin-Set l (n +ℕ 2))))
       ( comp-hom-Group
         ( symmetric-Group (raise-Fin-Set l (n +ℕ 2)))
         ( symmetric-Group (Fin-Set (n +ℕ 2)))
-        ( abstract-group-Concrete-Group (UU-Fin-Group (lsuc l) 2))
+        ( group-Concrete-Group (UU-Fin-Group (lsuc l) 2))
         ( comp-hom-Group
           ( symmetric-Group (Fin-Set (n +ℕ 2)))
           ( symmetric-Group (Fin-Set 2))
-          ( abstract-group-Concrete-Group (UU-Fin-Group (lsuc l) 2))
+          ( group-Concrete-Group (UU-Fin-Group (lsuc l) 2))
           ( symmetric-abstract-UU-fin-group-quotient-hom
             ( orientation-Complete-Undirected-Graph)
             ( even-difference-orientation-Complete-Undirected-Graph)