diff --git a/agda-unimath.agda-lib b/agda-unimath.agda-lib index 44045614215..24895407da0 100644 --- a/agda-unimath.agda-lib +++ b/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 diff --git a/src/analysis/series-metric-abelian-groups.lagda.md b/src/analysis/series-metric-abelian-groups.lagda.md index 1bb3d80a5e6..0d5cb90421a 100644 --- a/src/analysis/series-metric-abelian-groups.lagda.md +++ b/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) diff --git a/src/category-theory/large-categories.lagda.md b/src/category-theory/large-categories.lagda.md index b798eee3119..6b47dbd3e85 100644 --- a/src/category-theory/large-categories.lagda.md +++ b/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 diff --git a/src/category-theory/large-precategories.lagda.md b/src/category-theory/large-precategories.lagda.md index 4220dda23e8..553f6ef0720 100644 --- a/src/category-theory/large-precategories.lagda.md +++ b/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) diff --git a/src/commutative-algebra/formal-power-series-commutative-semirings.lagda.md b/src/commutative-algebra/formal-power-series-commutative-semirings.lagda.md index 96cd3315feb..c19182f02cc 100644 --- a/src/commutative-algebra/formal-power-series-commutative-semirings.lagda.md +++ b/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 diff --git a/src/foundation/dependent-pair-types.lagda.md b/src/foundation/dependent-pair-types.lagda.md index 2433065980d..9796580d4bb 100644 --- a/src/foundation/dependent-pair-types.lagda.md +++ b/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 diff --git a/src/foundation/large-dependent-pair-types.lagda.md b/src/foundation/large-dependent-pair-types.lagda.md index 3135d45bbc1..913644fae91 100644 --- a/src/foundation/large-dependent-pair-types.lagda.md +++ b/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 diff --git a/src/foundation/unit-type.lagda.md b/src/foundation/unit-type.lagda.md index 34a0415d7f3..2339dfed702 100644 --- a/src/foundation/unit-type.lagda.md +++ b/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 #-} diff --git a/src/globular-types/discrete-reflexive-globular-types.lagda.md b/src/globular-types/discrete-reflexive-globular-types.lagda.md index 9e45c68d208..69218b3f915 100644 --- a/src/globular-types/discrete-reflexive-globular-types.lagda.md +++ b/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 diff --git a/src/globular-types/reflexive-globular-types.lagda.md b/src/globular-types/reflexive-globular-types.lagda.md index 8eec1e2951a..cd5dada28d2 100644 --- a/src/globular-types/reflexive-globular-types.lagda.md +++ b/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: diff --git a/src/globular-types/transitive-globular-types.lagda.md b/src/globular-types/transitive-globular-types.lagda.md index 368bad45fc0..2b0f7aa7b51 100644 --- a/src/globular-types/transitive-globular-types.lagda.md +++ b/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 ``` diff --git a/src/order-theory/large-posets.lagda.md b/src/order-theory/large-posets.lagda.md index 5fbe47a8032..94cdb9bd40b 100644 --- a/src/order-theory/large-posets.lagda.md +++ b/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 diff --git a/src/order-theory/large-preorders.lagda.md b/src/order-theory/large-preorders.lagda.md index 34c91707425..d832ad2c9d9 100644 --- a/src/order-theory/large-preorders.lagda.md +++ b/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 diff --git a/src/order-theory/order-preserving-maps-large-preorders.lagda.md b/src/order-theory/order-preserving-maps-large-preorders.lagda.md index d9150512e77..38c5178e996 100644 --- a/src/order-theory/order-preserving-maps-large-preorders.lagda.md +++ b/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 diff --git a/src/wild-category-theory/colax-functors-noncoherent-large-omega-precategories.lagda.md b/src/wild-category-theory/colax-functors-noncoherent-large-omega-precategories.lagda.md index 714375f4a2b..1ffc3080558 100644 --- a/src/wild-category-theory/colax-functors-noncoherent-large-omega-precategories.lagda.md +++ b/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 ```