No-postfix-projections (#1240)

UniMath · Jan 26, 2025 · dc4a21a · dc4a21a
1 parent 77decd8
commit dc4a21a
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 7 deletions.
diff --git 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
+flags: --without-K --exact-split --no-import-sorts --auto-inline --no-require-unique-meta-solutions -WnoWithoutKFlagPrimEraseEquality --no-postfix-projections
diff --git a/src/order-theory/incidence-algebras.lagda.md b/src/order-theory/incidence-algebras.lagda.md
@@ -24,13 +24,13 @@ open import order-theory.posets
 
 ## Idea
 
-For a [locally finite poset](order-theory.locally-finite-posets.md) 'P' and
-[commutative ring](commutative-algebra.commutative-rings.md) 'R', there is a
-canonical 'R'-associative algebra whose underlying 'R'-module are the set-maps
-from the nonempty [intervals](order-theory.interval-subposets.md) of 'P' to 'R'
+For a [locally finite poset](order-theory.locally-finite-posets.md) `P` and
+[commutative ring](commutative-algebra.commutative-rings.md) `R`, there is a
+canonical `R`-associative algebra whose underlying `R`-module are the set-maps
+from the nonempty [intervals](order-theory.interval-subposets.md) of `P` to `R`
 (which we constructify as the inhabited intervals), and whose multiplication is
-given by a "convolution" of maps. This is the **incidence algebra** of 'P' over
-'R'.
+given by a "convolution" of maps. This is the **incidence algebra** of `P` over
+`R`.
 
 ## Definition