definition 2.14.1

src/HottBook/Chapter2.lagda.md

@@ -954,6 +954,18 @@ module theorem2∙13∙1 where
   theorem2∙13∙1 m n = encode m n , qinv-to-isequiv (mkQinv (decode m n) (backward m n) (forward m n))
 ```
 
+## 2.14 Example: equality of structures
+
+### Definition 2.14.1
+
+```
+SemigroupStr : (A : Set l) → Set l
+SemigroupStr A = Σ (A → A → A) (λ m → (x y z : A) → m x (m y z) ≡ m (m x y) z)
+
+Semigroup : Set (lsuc l)
+Semigroup {l = l} = Σ (Set l) SemigroupStr
+```
+
 ## 2.15 Universal properties
 
 Definition 2.15.1