Turn off η-equality by default

agda-unimath.agda-lib

@@ -1,3 +1,3 @@
 name: agda-unimath
 include: src
-flags: --without-K --exact-split --no-import-sorts --auto-inline --no-require-unique-meta-solutions -WnoWithoutKFlagPrimEraseEquality --no-postfix-projections
+flags: --without-K --exact-split --no-import-sorts --auto-inline --no-require-unique-meta-solutions -WnoWithoutKFlagPrimEraseEquality --no-postfix-projections --no-eta-equality

src/analysis/series-metric-abelian-groups.lagda.md

@@ -46,6 +46,7 @@ sequence of their terms.
 
 ```agda
 record series-Metric-Ab {l1 l2 : Level} (G : Metric-Ab l1 l2) : UU l1 where
+  eta-equality
   constructor series-terms-Metric-Ab
   field
     term-series-Metric-Ab : sequence (type-Metric-Ab G)

src/category-theory/large-categories.lagda.md

@@ -55,6 +55,9 @@ is-large-category-Large-Precategory C =
 record
   Large-Category (α : Level → Level) (β : Level → Level → Level) : UUω
   where
+
+  eta-equality
+
   constructor
     make-Large-Category
 

src/category-theory/large-precategories.lagda.md

@@ -35,6 +35,8 @@ be done with Σ-types, we must use a record type.)
 record
   Large-Precategory (α : Level → Level) (β : Level → Level → Level) : UUω where
 
+  eta-equality
+
   field
     obj-Large-Precategory :
       (l : Level) → UU (α l)

src/commutative-algebra/formal-power-series-commutative-semirings.lagda.md

@@ -54,6 +54,8 @@ record
     {l : Level} (R : Commutative-Semiring l) : UU l
   where
 
+  eta-equality
+
   constructor formal-power-series-coefficients-Commutative-Semiring
 
   field

src/foundation/dependent-pair-types.lagda.md

@@ -26,6 +26,7 @@ Consider a type family `B` over `A`. The
 
 ```agda
 record Σ {l1 l2 : Level} (A : UU l1) (B : A → UU l2) : UU (l1 ⊔ l2) where
+  eta-equality
   constructor pair
   field
     pr1 : A

src/foundation/large-dependent-pair-types.lagda.md

@@ -23,6 +23,7 @@ depends on the first component.
 
 ```agda
 record Σω (A : UUω) (B : A → UUω) : UUω where
+  eta-equality
   constructor pairω
   field
     prω1 : A

src/foundation/unit-type.lagda.md

@@ -38,6 +38,7 @@ The **unit type** is a type inductively generated by a single point.
 
 ```agda
 record unit : UU lzero where
+  eta-equality
   instance constructor star
 
 {-# BUILTIN UNIT unit #-}

src/globular-types/discrete-reflexive-globular-types.lagda.md

@@ -73,6 +73,8 @@ record
     (l1 l2 : Level) : UU (lsuc l1 ⊔ lsuc l2)
   where
 
+  eta-equality
+
   field
     reflexive-globular-type-Discrete-Reflexive-Globular-Type :
       Reflexive-Globular-Type l1 l2

src/globular-types/reflexive-globular-types.lagda.md

@@ -121,6 +121,8 @@ module _
 record
   Reflexive-Globular-Type (l1 l2 : Level) : UU (lsuc l1 ⊔ lsuc l2)
   where
+
+  eta-equality
 ```
 
 The underlying globular type of a reflexive globular type:

src/globular-types/transitive-globular-types.lagda.md

@@ -110,6 +110,8 @@ record
     (l1 l2 : Level) : UU (lsuc l1 ⊔ lsuc l2)
   where
 
+  eta-equality
+
   constructor
     make-Transitive-Globular-Type
 ```

src/order-theory/large-posets.lagda.md

@@ -41,7 +41,9 @@ is antisymmetric.
 
 ```agda
 record
-  Large-Poset (α : Level → Level) (β : Level → Level → Level) : UUω where
+  Large-Poset (α : Level → Level) (β : Level → Level → Level) : UUω
+  where
+  eta-equality
   constructor
     make-Large-Poset
   field

src/order-theory/large-preorders.lagda.md

@@ -36,7 +36,9 @@ agda-unimath naturally arise as large preorders.
 
 ```agda
 record
-  Large-Preorder (α : Level → Level) (β : Level → Level → Level) : UUω where
+  Large-Preorder (α : Level → Level) (β : Level → Level → Level) : UUω
+  where
+  eta-equality
   constructor
     make-Large-Preorder
   field

src/order-theory/order-preserving-maps-large-preorders.lagda.md

@@ -65,6 +65,7 @@ module _
 
   record hom-Large-Preorder : UUω
     where
+    eta-equality
     constructor
       make-hom-Large-Preorder
     field

src/wild-category-theory/colax-functors-noncoherent-large-omega-precategories.lagda.md

@@ -209,6 +209,8 @@ record
   (ℬ : Noncoherent-Large-ω-Precategory α2 β2) : UUω
   where
 
+  eta-equality
+
   constructor
     make-colax-functor-Noncoherent-Large-ω-Precategory
 ```