Adding explicit zero algebras (UniMath#1095)

Added initial work for the zero ring and zero abelian group, along with
proofs of their uniqueness up to contractible type. Remaining work is
refactoring for the rest of the zero algebras along the way and the
final uniqueness proof by SIP.

CONTRIBUTORS.toml

@@ -237,3 +237,8 @@ github = "wrest64"
 displayName = "Ulrik Buchholtz"
 usernames = [ "Ulrik Buchholtz" ]
 github = "UlrikBuchholtz"
+
+[[contributors]]
+displayName = "Garrett Figueroa"
+usernames = [ "Garrett Figueroa", "djspacewhale" ]
+github = "djspacewhale"

src/commutative-algebra/trivial-commutative-rings.lagda.md

@@ -8,13 +8,23 @@ module commutative-algebra.trivial-commutative-rings where
 
 ```agda
 open import commutative-algebra.commutative-rings
+open import commutative-algebra.isomorphisms-commutative-rings
 
 open import foundation.contractible-types
+open import foundation.dependent-pair-types
 open import foundation.negation
 open import foundation.propositions
 open import foundation.sets
+open import foundation.structure-identity-principle
+open import foundation.unit-type
 open import foundation.universe-levels
 
+open import foundation-core.identity-types
+
+open import group-theory.abelian-groups
+open import group-theory.trivial-groups
+
+open import ring-theory.rings
 open import ring-theory.trivial-rings
 ```
 
@@ -75,3 +85,32 @@ is-contr-is-trivial-Commutative-Ring :
 is-contr-is-trivial-Commutative-Ring A p =
   is-contr-is-trivial-Ring (ring-Commutative-Ring A) p
 ```
+
+### The trivial ring
+
+```agda
+trivial-Ring : Ring lzero
+pr1 trivial-Ring = trivial-Ab
+pr1 (pr1 (pr2 trivial-Ring)) x y = star
+pr2 (pr1 (pr2 trivial-Ring)) x y z = refl
+pr1 (pr1 (pr2 (pr2 trivial-Ring))) = star
+pr1 (pr2 (pr1 (pr2 (pr2 trivial-Ring)))) star = refl
+pr2 (pr2 (pr1 (pr2 (pr2 trivial-Ring)))) star = refl
+pr2 (pr2 (pr2 trivial-Ring)) = (λ a b c → refl) , (λ a b c → refl)
+
+is-commutative-trivial-Ring : is-commutative-Ring trivial-Ring
+is-commutative-trivial-Ring x y = refl
+
+trivial-Commutative-Ring : Commutative-Ring lzero
+trivial-Commutative-Ring = (trivial-Ring , is-commutative-trivial-Ring)
+
+is-trivial-trivial-Commutative-Ring :
+  is-trivial-Commutative-Ring trivial-Commutative-Ring
+is-trivial-trivial-Commutative-Ring = refl
+```
+
+### The type of trivial rings is contractible
+
+To-do: complete proof of uniqueness of the zero ring using SIP, ideally refactor
+code to do zero algebras all along the chain to prettify and streamline future
+work

src/group-theory/trivial-groups.lagda.md

@@ -9,10 +9,17 @@ module group-theory.trivial-groups where
 ```agda
 open import foundation.contractible-types
 open import foundation.dependent-pair-types
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.propositions
+open import foundation.raising-universe-levels
+open import foundation.structure-identity-principle
+open import foundation.unit-type
 open import foundation.universe-levels
 
+open import group-theory.abelian-groups
+open import group-theory.full-subgroups
 open import group-theory.groups
 open import group-theory.subgroups
 open import group-theory.trivial-subgroups
@@ -40,9 +47,24 @@ module _
 
   is-trivial-Group : UU l1
   is-trivial-Group = type-Prop is-trivial-prop-Group
+```
+
+### The type of trivial groups
+
+```agda
+Trivial-Group : (l : Level) → UU (lsuc l)
+Trivial-Group l = Σ (Group l) is-trivial-Group
+```
+
+### The trivial group
 
-  is-prop-is-trivial-Group : is-prop is-trivial-Group
-  is-prop-is-trivial-Group = is-prop-type-Prop is-trivial-prop-Group
+```agda
+trivial-Group : Group lzero
+pr1 (pr1 trivial-Group) = unit-Set
+pr1 (pr2 (pr1 trivial-Group)) x y = star
+pr2 (pr2 (pr1 trivial-Group)) x y z = refl
+pr1 (pr2 trivial-Group) = (star , (refl-htpy , refl-htpy))
+pr2 (pr2 trivial-Group) = ((λ x → star) , refl-htpy , refl-htpy)
 ```
 
 ## Properties
@@ -71,3 +93,13 @@ module _
               ( contains-unit-Subgroup G (trivial-Subgroup G))
               ( eq-is-contr H)))
 ```
+
+### The trivial group is abelian
+
+```agda
+is-abelian-trivial-Group : is-abelian-Group trivial-Group
+is-abelian-trivial-Group x y = refl
+
+trivial-Ab : Ab lzero
+trivial-Ab = (trivial-Group , is-abelian-trivial-Group)
+```