diff --git a/src/category-theory/adjunctions-large-precategories.lagda.md b/src/category-theory/adjunctions-large-precategories.lagda.md
index 79a716a467..ba63d12361 100644
--- a/src/category-theory/adjunctions-large-precategories.lagda.md
+++ b/src/category-theory/adjunctions-large-precategories.lagda.md
@@ -29,7 +29,7 @@ Let `C` and `D` be two large precategories. Two functors `F : C → D` and
 - for every pair of morhpisms `f : X₂ → X₁` and `g : Y₁ → Y₂` the following
   square commutes:
 
-```md
+```text
                        ϕ X₁ Y₁
        hom X₁ (G Y₁) --------> hom (F X₁) Y₁
             |                        |
diff --git a/src/commutative-algebra/binomial-theorem-commutative-rings.lagda.md b/src/commutative-algebra/binomial-theorem-commutative-rings.lagda.md
index a7e5130a90..02c0479193 100644
--- a/src/commutative-algebra/binomial-theorem-commutative-rings.lagda.md
+++ b/src/commutative-algebra/binomial-theorem-commutative-rings.lagda.md
@@ -35,8 +35,8 @@ open import univalent-combinatorics.standard-finite-types
 The **binomial theorem** in commutative rings asserts that for any two elements
 `x` and `y` of a commutative ring `A` and any natural number `n`, we have
 
-```md
-  (x + y)ⁿ = ∑\_{0 ≤ i < n+1} (n choose i) xⁱ yⁿ⁻ⁱ.
+```text
+  (x + y)ⁿ = ∑_{0 ≤ i < n+1} (n choose i) xⁱ yⁿ⁻ⁱ.
 ```
 
 ## Definitions
diff --git a/src/commutative-algebra/binomial-theorem-commutative-semirings.lagda.md b/src/commutative-algebra/binomial-theorem-commutative-semirings.lagda.md
index bb7b5a11b8..1b9eae61bb 100644
--- a/src/commutative-algebra/binomial-theorem-commutative-semirings.lagda.md
+++ b/src/commutative-algebra/binomial-theorem-commutative-semirings.lagda.md
@@ -35,8 +35,8 @@ The **binomial theorem** in commutative semirings asserts that for any two
 elements `x` and `y` of a commutative semiring `A` and any natural number `n`,
 we have
 
-```md
-  (x + y)ⁿ = ∑\_{0 ≤ i < n+1} (n choose i) xⁱ yⁿ⁻ⁱ.
+```text
+  (x + y)ⁿ = ∑_{0 ≤ i < n+1} (n choose i) xⁱ yⁿ⁻ⁱ.
 ```
 
 ## Definitions
diff --git a/src/elementary-number-theory/based-induction-natural-numbers.lagda.md b/src/elementary-number-theory/based-induction-natural-numbers.lagda.md
index d6dfff288a..6ca59ad1cb 100644
--- a/src/elementary-number-theory/based-induction-natural-numbers.lagda.md
+++ b/src/elementary-number-theory/based-induction-natural-numbers.lagda.md
@@ -25,7 +25,7 @@ family `P` of types over `ℕ` and any natural number `k : ℕ`, equipped with
 1. An element `p0 : P k`
 2. A function `pS : (x : ℕ) → k ≤-ℕ x → P x → P (x + 1)` there is a function
 
-```md
+```text
   based-ind-ℕ k P p0 pS : (x : ℕ) → k ≤-ℕ x → P x
 ```
 
diff --git a/src/elementary-number-theory/based-strong-induction-natural-numbers.lagda.md b/src/elementary-number-theory/based-strong-induction-natural-numbers.lagda.md
index 3c7260d443..2919021dc7 100644
--- a/src/elementary-number-theory/based-strong-induction-natural-numbers.lagda.md
+++ b/src/elementary-number-theory/based-strong-induction-natural-numbers.lagda.md
@@ -34,7 +34,7 @@ numbers equipped with
    `pS : (x : ℕ) → k ≤-ℕ x → ((y : ℕ) → k ≤-ℕ y ≤-ℕ x → P y) → P (x + 1)` there
    is a function
 
-```md
+```text
   f := based-strong-ind-ℕ k P p0 pS : (x : ℕ) → k ≤-ℕ x → P k
 ```
 
diff --git a/src/elementary-number-theory/bezouts-lemma-natural-numbers.lagda.md b/src/elementary-number-theory/bezouts-lemma-natural-numbers.lagda.md
index 811666237b..9893d0e23e 100755
--- a/src/elementary-number-theory/bezouts-lemma-natural-numbers.lagda.md
+++ b/src/elementary-number-theory/bezouts-lemma-natural-numbers.lagda.md
@@ -49,7 +49,7 @@ Bezout's lemma shows that for any two natural numbers `x` and `y` there exist
 `k` and `l` such that `dist-ℕ (kx,ly) = gcd(x,y)`. To prove this, note that the
 predicate `P : ℕ → UU lzero` given by
 
-```md
+```text
   P z := Σ (k : ℕ), Σ (l : ℕ), dist-ℕ (kx, ly) = z
 ```
 
diff --git a/src/elementary-number-theory/binomial-theorem-integers.lagda.md b/src/elementary-number-theory/binomial-theorem-integers.lagda.md
index b893d34f04..61d2d8a7f6 100644
--- a/src/elementary-number-theory/binomial-theorem-integers.lagda.md
+++ b/src/elementary-number-theory/binomial-theorem-integers.lagda.md
@@ -32,7 +32,7 @@ open import univalent-combinatorics.standard-finite-types
 The binomial theorem for the integers asserts that for any two integers `x` and
 `y` and any natural number `n`, we have
 
-```md
+```text
   (x + y)ⁿ = ∑_{0 ≤ i < n+1} (n choose i) xⁱ yⁿ⁻ⁱ.
 ```
 
diff --git a/src/elementary-number-theory/binomial-theorem-natural-numbers.lagda.md b/src/elementary-number-theory/binomial-theorem-natural-numbers.lagda.md
index 866345e559..17ded707df 100644
--- a/src/elementary-number-theory/binomial-theorem-natural-numbers.lagda.md
+++ b/src/elementary-number-theory/binomial-theorem-natural-numbers.lagda.md
@@ -31,7 +31,7 @@ open import univalent-combinatorics.standard-finite-types
 The binomial theorem for natural numbers asserts that for any two natural
 numbers `x` and `y` and any natural number `n`, we have
 
-```md
+```text
   (x + y)ⁿ = ∑_{0 ≤ i < n+1} (n choose i) xⁱ yⁿ⁻ⁱ.
 ```
 
diff --git a/src/elementary-number-theory/cofibonacci.lagda.md b/src/elementary-number-theory/cofibonacci.lagda.md
index bed5481ac2..3801e8882c 100644
--- a/src/elementary-number-theory/cofibonacci.lagda.md
+++ b/src/elementary-number-theory/cofibonacci.lagda.md
@@ -31,7 +31,7 @@ open import foundation.universe-levels
 The [**cofibonacci sequence**][1] is the unique function G : ℕ → ℕ satisfying
 the property that
 
-```md
+```text
   div-ℕ (G m) n ↔ div-ℕ m (Fibonacci-ℕ n).
 ```
 
diff --git a/src/elementary-number-theory/divisibility-integers.lagda.md b/src/elementary-number-theory/divisibility-integers.lagda.md
index 963317b1da..672356c1d7 100644
--- a/src/elementary-number-theory/divisibility-integers.lagda.md
+++ b/src/elementary-number-theory/divisibility-integers.lagda.md
@@ -37,7 +37,7 @@ An integer `m` is said to **divide** an integer `n` if there exists an integer
 `k` equipped with an identification `km ＝ n`. Using the Curry-Howard
 interpretation of logic into type theory, we express divisibility as follows:
 
-```md
+```text
   div-ℤ m n := Σ (k : ℤ), k *ℤ m ＝ n.
 ```
 
diff --git a/src/elementary-number-theory/divisibility-natural-numbers.lagda.md b/src/elementary-number-theory/divisibility-natural-numbers.lagda.md
index 6a22ec8c7c..3c49d732b2 100644
--- a/src/elementary-number-theory/divisibility-natural-numbers.lagda.md
+++ b/src/elementary-number-theory/divisibility-natural-numbers.lagda.md
@@ -35,7 +35,7 @@ a natural number `k` equipped with an identification `km ＝ n`. Using the
 Curry-Howard interpretation of logic into type theory, we express divisibility
 as follows:
 
-```md
+```text
   div-ℕ m n := Σ (k : ℕ), k *ℕ m ＝ n.
 ```
 
diff --git a/src/elementary-number-theory/euclidean-division-natural-numbers.lagda.md b/src/elementary-number-theory/euclidean-division-natural-numbers.lagda.md
index ce2fc617c1..73878d7908 100644
--- a/src/elementary-number-theory/euclidean-division-natural-numbers.lagda.md
+++ b/src/elementary-number-theory/euclidean-division-natural-numbers.lagda.md
@@ -38,7 +38,7 @@ unique natural number `r < d` such that `kd + r = n`.
 The following definition produces for each `k : ℕ` a sequence of sequences as
 follows:
 
-```md
+```text
     This is column k
       ↓
   0,…,0,0,0,0,0,0,0,…  -- The sequence at row 0 is the constant sequence
diff --git a/src/elementary-number-theory/initial-segments-natural-numbers.lagda.md b/src/elementary-number-theory/initial-segments-natural-numbers.lagda.md
index 9ddcf65803..4de715f99d 100644
--- a/src/elementary-number-theory/initial-segments-natural-numbers.lagda.md
+++ b/src/elementary-number-theory/initial-segments-natural-numbers.lagda.md
@@ -25,7 +25,7 @@ open import foundation.universe-levels
 An **initial segment** of the natural numbers is a subtype `P : ℕ → Prop` such
 that the implication
 
-```md
+```text
   P (n + 1) → P n
 ```
 
diff --git a/src/elementary-number-theory/kolakoski-sequence.lagda.md b/src/elementary-number-theory/kolakoski-sequence.lagda.md
index 86794d3ab3..fbc5410387 100644
--- a/src/elementary-number-theory/kolakoski-sequence.lagda.md
+++ b/src/elementary-number-theory/kolakoski-sequence.lagda.md
@@ -22,14 +22,14 @@ open import foundation.dependent-pair-types
 
 The Kolakoski sequence
 
-```md
+```text
 1,2,2,1,1,2,1,2,2,1,2,2,1,1,...
 ```
 
 is a self-referential sequence of `1`s and `2`s which is the flattening of a
 sequence
 
-```md
+```text
 (1),(2,2),(1,1),(2),(1),(2,2),(1,1)
 ```
 
diff --git a/src/elementary-number-theory/multiset-coefficients.lagda.md b/src/elementary-number-theory/multiset-coefficients.lagda.md
index 2cbb21d43b..211771b40d 100644
--- a/src/elementary-number-theory/multiset-coefficients.lagda.md
+++ b/src/elementary-number-theory/multiset-coefficients.lagda.md
@@ -19,7 +19,7 @@ The multiset coefficients count the number of multisets of size `k` of elements
 of a set of size `n`. In oter words, it counts the number of connected componets
 of the type
 
-```md
+```text
   Σ (A : Fin n → 𝔽), ∥ Fin k ≃ Σ (i : Fin n), A i ∥.
 ```
 
diff --git a/src/finite-group-theory/delooping-sign-homomorphism.lagda.md b/src/finite-group-theory/delooping-sign-homomorphism.lagda.md
index ac71151b28..00d7945ccd 100644
--- a/src/finite-group-theory/delooping-sign-homomorphism.lagda.md
+++ b/src/finite-group-theory/delooping-sign-homomorphism.lagda.md
@@ -84,7 +84,7 @@ The delooping of a group homomorphism `f : G → H` is a pointed map
 `Bf : BG → BH` equiped with an homotopy witnessing that the following square
 commutes :
 
-```md
+```text
         f
   G --------> H
   |           |
diff --git a/src/foundation-core/commuting-3-simplices-of-homotopies.lagda.md b/src/foundation-core/commuting-3-simplices-of-homotopies.lagda.md
index 6d6c7daf9d..2f413429ed 100644
--- a/src/foundation-core/commuting-3-simplices-of-homotopies.lagda.md
+++ b/src/foundation-core/commuting-3-simplices-of-homotopies.lagda.md
@@ -19,7 +19,7 @@ open import foundation-core.universe-levels
 
 A commuting 3-simplex of homotopies is a commuting diagram of the form
 
-```md
+```text
   f ----------> g
   |  \       ^  |
   |    \   /    |
diff --git a/src/foundation-core/commuting-3-simplices-of-maps.lagda.md b/src/foundation-core/commuting-3-simplices-of-maps.lagda.md
index 258725c113..4bd4457058 100644
--- a/src/foundation-core/commuting-3-simplices-of-maps.lagda.md
+++ b/src/foundation-core/commuting-3-simplices-of-maps.lagda.md
@@ -19,7 +19,7 @@ open import foundation-core.universe-levels
 
 A commuting 3-simplex is a commuting diagram of the form
 
-```md
+```text
   A ----------> B
   |  \       ^  |
   |    \   /    |
diff --git a/src/foundation-core/commuting-cubes-of-maps.lagda.md b/src/foundation-core/commuting-cubes-of-maps.lagda.md
index f91cd3d40d..f3f6ef8662 100644
--- a/src/foundation-core/commuting-cubes-of-maps.lagda.md
+++ b/src/foundation-core/commuting-cubes-of-maps.lagda.md
@@ -24,7 +24,7 @@ open import foundation-core.universe-levels
 We specify the type of the homotopy witnessing that a cube commutes. Imagine
 that the cube is presented as a lattice
 
-```md
+```text
             *
           / | \
          /  |  \
diff --git a/src/foundation-core/commuting-squares-of-maps.lagda.md b/src/foundation-core/commuting-squares-of-maps.lagda.md
index 1861cd5e70..2cec5bd180 100644
--- a/src/foundation-core/commuting-squares-of-maps.lagda.md
+++ b/src/foundation-core/commuting-squares-of-maps.lagda.md
@@ -23,7 +23,7 @@ open import foundation-core.universe-levels
 
 A square of maps
 
-```md
+```text
   A ------> X
   |         |
   |         |
diff --git a/src/foundation-core/commuting-triangles-of-homotopies.lagda.md b/src/foundation-core/commuting-triangles-of-homotopies.lagda.md
index 0601a87363..d86703bcdf 100644
--- a/src/foundation-core/commuting-triangles-of-homotopies.lagda.md
+++ b/src/foundation-core/commuting-triangles-of-homotopies.lagda.md
@@ -20,7 +20,7 @@ open import foundation-core.universe-levels
 
 A triangle of homotopies of maps
 
-```md
+```text
  f ----> g
   \     /
    \   /
diff --git a/src/foundation-core/commuting-triangles-of-maps.lagda.md b/src/foundation-core/commuting-triangles-of-maps.lagda.md
index 9500645def..f1df78636a 100644
--- a/src/foundation-core/commuting-triangles-of-maps.lagda.md
+++ b/src/foundation-core/commuting-triangles-of-maps.lagda.md
@@ -19,7 +19,7 @@ open import foundation-core.universe-levels
 
 A triangle of maps
 
-```md
+```text
  A ----> B
   \     /
    \   /
diff --git a/src/foundation-core/cones-over-cospans.lagda.md b/src/foundation-core/cones-over-cospans.lagda.md
index a7e6a58b18..617ff9b952 100644
--- a/src/foundation-core/cones-over-cospans.lagda.md
+++ b/src/foundation-core/cones-over-cospans.lagda.md
@@ -28,7 +28,7 @@ A cone on a cospan `A --f--> X <--g-- B` with vertex `C` is a triple `(p,q,H)`
 consisting of a map `p : C → A`, a map `q : C → B`, and a homotopy `H`
 witnessing that the square
 
-```md
+```text
       q
   C -----> B
   |        |
diff --git a/src/foundation-core/equality-fibers-of-maps.lagda.md b/src/foundation-core/equality-fibers-of-maps.lagda.md
index 8f2f3e0917..8c564a0889 100644
--- a/src/foundation-core/equality-fibers-of-maps.lagda.md
+++ b/src/foundation-core/equality-fibers-of-maps.lagda.md
@@ -34,7 +34,7 @@ action on identifications of `f`.
 For any map `f : A → B` any `b : B` and any `x y : fib f b`, there is an
 equivalence
 
-```md
+```text
 (x ＝ y) ≃ fib (ap f) ((pr2 x) ∙ (inv (pr2 y)))
 ```
 
diff --git a/src/foundation-core/equivalences.lagda.md b/src/foundation-core/equivalences.lagda.md
index f8234ca2bf..d6cb1f29af 100644
--- a/src/foundation-core/equivalences.lagda.md
+++ b/src/foundation-core/equivalences.lagda.md
@@ -463,7 +463,7 @@ is-equiv-equiv' {f = f} {g} i j H K =
 
 We will assume a commuting square
 
-```md
+```text
           h
     A --------> C
     |           |
@@ -562,7 +562,7 @@ module _
 
 Equivalences can be constructed by equational reasoning in the following way:
 
-```md
+```text
 equivalence-reasoning
   X ≃ Y by equiv-1
     ≃ Z by equiv-2
diff --git a/src/foundation-core/homotopies.lagda.md b/src/foundation-core/homotopies.lagda.md
index da335ba23c..0ca4bde54f 100644
--- a/src/foundation-core/homotopies.lagda.md
+++ b/src/foundation-core/homotopies.lagda.md
@@ -348,7 +348,7 @@ module _
 
 Homotopies can be constructed by equational reasoning in the following way:
 
-```md
+```text
 homotopy-reasoning
   f ~ g by htpy-1
     ~ h by htpy-2
diff --git a/src/foundation-core/identity-types.lagda.md b/src/foundation-core/identity-types.lagda.md
index 6a44682de2..2a0f67b0ea 100644
--- a/src/foundation-core/identity-types.lagda.md
+++ b/src/foundation-core/identity-types.lagda.md
@@ -469,7 +469,7 @@ ap-binary-concat f refl refl refl refl = refl
 
 Identifications can be constructed by equational reasoning in the following way:
 
-```md
+```text
 equational-reasoning
   x ＝ y by eq-1
     ＝ z by eq-2
diff --git a/src/foundation-core/logical-equivalences.lagda.md b/src/foundation-core/logical-equivalences.lagda.md
index 5fedd25c94..ac0c74494b 100644
--- a/src/foundation-core/logical-equivalences.lagda.md
+++ b/src/foundation-core/logical-equivalences.lagda.md
@@ -120,7 +120,7 @@ module _
 Logical equivalences can be constructed by equational reasoning in the following
 way:
 
-```md
+```text
 logical-equivalence-reasoning
   X ↔ Y by equiv-1
     ↔ Z by equiv-2
diff --git a/src/foundation-core/morphisms-cospans.lagda.md b/src/foundation-core/morphisms-cospans.lagda.md
index b2dfc8c033..5e197c2258 100644
--- a/src/foundation-core/morphisms-cospans.lagda.md
+++ b/src/foundation-core/morphisms-cospans.lagda.md
@@ -24,7 +24,7 @@ open import foundation-core.universe-levels
 
 A morphism of cospans is a commuting diagram of the form
 
-```md
+```text
   A -----> X <----- B
   |        |        |
   |        |        |
diff --git a/src/foundation-core/propositions.lagda.md b/src/foundation-core/propositions.lagda.md
index c305583820..ab2e572b99 100644
--- a/src/foundation-core/propositions.lagda.md
+++ b/src/foundation-core/propositions.lagda.md
@@ -54,7 +54,7 @@ module _
 We prove here only that any contractible type is a proposition. The fact that
 the empty type and the unit type are propositions can be found in
 
-```md
+```text
 foundation.empty-types
 foundation.unit-type
 ```
diff --git a/src/foundation/arithmetic-law-coproduct-and-sigma-decompositions.lagda.md b/src/foundation/arithmetic-law-coproduct-and-sigma-decompositions.lagda.md
index 9f9e5acb51..aee657b134 100644
--- a/src/foundation/arithmetic-law-coproduct-and-sigma-decompositions.lagda.md
+++ b/src/foundation/arithmetic-law-coproduct-and-sigma-decompositions.lagda.md
@@ -33,7 +33,7 @@ open import foundation-core.universe-levels
 
 Let `X` be a type, we have the following equivalence :
 
-```md
+```text
  Σ ( (U , V , e) : Relaxed-Σ-Decomposition X)
    ( binary-coproduct-Decomposition U) ≃
  Σ ( (A , B , e) : binary-coproduct-Decomposition X)
diff --git a/src/foundation/binary-transport.lagda.md b/src/foundation/binary-transport.lagda.md
index bd4cc27504..1d4a0d8989 100644
--- a/src/foundation/binary-transport.lagda.md
+++ b/src/foundation/binary-transport.lagda.md
@@ -21,7 +21,7 @@ open import foundation-core.universe-levels
 Given a binary relation `B : A → A → UU` and identifications `p : x ＝ x'` and
 `q : y ＝ y'` in `A`, the binary transport of `B` is an operation
 
-```md
+```text
   binary-tr B p q : B x y → B x' y'
 ```
 
diff --git a/src/foundation/commuting-squares-of-identifications.lagda.md b/src/foundation/commuting-squares-of-identifications.lagda.md
index 0108e31dda..96e2c16709 100644
--- a/src/foundation/commuting-squares-of-identifications.lagda.md
+++ b/src/foundation/commuting-squares-of-identifications.lagda.md
@@ -19,7 +19,7 @@ open import foundation-core.universe-levels
 
 A square of identifications
 
-```md
+```text
           top
       x ------- y
       |         |
diff --git a/src/foundation/commuting-triangles-of-maps.lagda.md b/src/foundation/commuting-triangles-of-maps.lagda.md
index c604d32117..c38fc84909 100644
--- a/src/foundation/commuting-triangles-of-maps.lagda.md
+++ b/src/foundation/commuting-triangles-of-maps.lagda.md
@@ -22,7 +22,7 @@ open import foundation-core.universe-levels
 
 A triangle of maps
 
-```md
+```text
  A ----> B
   \     /
    \   /
diff --git a/src/foundation/descent-equivalences.lagda.md b/src/foundation/descent-equivalences.lagda.md
index 87ab434ae9..a013c44593 100644
--- a/src/foundation/descent-equivalences.lagda.md
+++ b/src/foundation/descent-equivalences.lagda.md
@@ -24,7 +24,7 @@ open import foundation-core.universe-levels
 The descent property of equivalences is a somewhat degenerate form of a descent
 property. It asserts that in a commuting diagram of the form
 
-```md
+```text
      p        q
  A -----> B -----> C
  |        |        |
diff --git a/src/foundation/epimorphisms-with-respect-to-truncated-types.lagda.md b/src/foundation/epimorphisms-with-respect-to-truncated-types.lagda.md
index de33dedec0..113971539c 100644
--- a/src/foundation/epimorphisms-with-respect-to-truncated-types.lagda.md
+++ b/src/foundation/epimorphisms-with-respect-to-truncated-types.lagda.md
@@ -29,7 +29,7 @@ open import foundation-core.universe-levels
 A map `f : A → B` is said to be a **`k`-epimorphism** if the precomposition
 function
 
-```md
+```text
   - ∘ f : (B → X) → (A → X)
 ```
 
diff --git a/src/foundation/epimorphisms.lagda.md b/src/foundation/epimorphisms.lagda.md
index 7d26a80271..db87b50a46 100644
--- a/src/foundation/epimorphisms.lagda.md
+++ b/src/foundation/epimorphisms.lagda.md
@@ -19,7 +19,7 @@ open import foundation-core.universe-levels
 A map `f : A → B` is said to be an **epimorphism** if the precomposition
 function
 
-```md
+```text
   - ∘ f : (B → X) → (A → X)
 ```
 
diff --git a/src/foundation/exponents-set-quotients.lagda.md b/src/foundation/exponents-set-quotients.lagda.md
index a03ef42bfe..834ab14c24 100644
--- a/src/foundation/exponents-set-quotients.lagda.md
+++ b/src/foundation/exponents-set-quotients.lagda.md
@@ -37,7 +37,7 @@ open import foundation-core.universe-levels
 Given a type `A` equipped with an equivalence relation `R` and a type `X`, the
 set quotient
 
-```md
+```text
   (X → A) / ~
 ```
 
@@ -46,7 +46,7 @@ embedding for every `X`, `A`, and `R` if and only if the axiom of choice holds.
 
 Consequently, we get embeddings
 
-```md
+```text
   ((hom-Eq-Rel R S) / ~) ↪ ((A/R) → (B/S))
 ```
 
diff --git a/src/foundation/fibered-equivalences.lagda.md b/src/foundation/fibered-equivalences.lagda.md
index 0b36951a00..d870a689c2 100644
--- a/src/foundation/fibered-equivalences.lagda.md
+++ b/src/foundation/fibered-equivalences.lagda.md
@@ -30,7 +30,7 @@ open import foundation-core.universe-levels
 
 A fibered equivalence is a fibered map
 
-```md
+```text
        h
   A -------> B
   |          |
diff --git a/src/foundation/fibered-involutions.lagda.md b/src/foundation/fibered-involutions.lagda.md
index 71198970f8..0e31181ed6 100644
--- a/src/foundation/fibered-involutions.lagda.md
+++ b/src/foundation/fibered-involutions.lagda.md
@@ -24,7 +24,7 @@ open import foundation-core.universe-levels
 
 A fibered involution is a fibered map
 
-```md
+```text
        h
   A -------> A
   |          |
diff --git a/src/foundation/fibered-maps.lagda.md b/src/foundation/fibered-maps.lagda.md
index fb77c6111e..324bf7ee38 100644
--- a/src/foundation/fibered-maps.lagda.md
+++ b/src/foundation/fibered-maps.lagda.md
@@ -34,7 +34,7 @@ open import foundation-core.universe-levels
 
 Consider a diagram of the form
 
-```md
+```text
   A         B
   |         |
  f|         |g
diff --git a/src/foundation/partitions.lagda.md b/src/foundation/partitions.lagda.md
index 614601d4dc..ee599d3dca 100644
--- a/src/foundation/partitions.lagda.md
+++ b/src/foundation/partitions.lagda.md
@@ -45,7 +45,7 @@ open import foundation-core.universe-levels
 A partition of a type `A` is a subset `P` of the type of inhabited subsets of
 `A` such that for each `a : A` the type
 
-```md
+```text
   Σ (Q : inhabited-subtype (A)), P(Q) × Q(a)
 ```
 
diff --git a/src/foundation/projective-types.lagda.md b/src/foundation/projective-types.lagda.md
index f1aab3c607..326b3d9389 100644
--- a/src/foundation/projective-types.lagda.md
+++ b/src/foundation/projective-types.lagda.md
@@ -26,14 +26,14 @@ open import foundation-core.universe-levels
 A type `X` is said to be **set-projective** if for every surjective map
 `f : A → B` into a set `B` the postcomposition function
 
-```md
+```text
   (X → A) → (X → B)
 ```
 
 is surjective. This is equivalent to the condition that for every equivalence
 relation `R` on a type `A` the natural map
 
-```md
+```text
   (X → A)/~ → (X → A/R)
 ```
 
diff --git a/src/foundation/shifting-sequences.lagda.md b/src/foundation/shifting-sequences.lagda.md
index f992351e3d..27337c4ebd 100644
--- a/src/foundation/shifting-sequences.lagda.md
+++ b/src/foundation/shifting-sequences.lagda.md
@@ -19,7 +19,7 @@ open import foundation-core.universe-levels
 Given a sequence `f : ℕ → A` and an element `a : A` we define
 `shift-ℕ a f : ℕ → A` by
 
-```md
+```text
   shift-ℕ a f zero-ℕ := a
   shift-ℕ a f (succ-ℕ n) := f n
 ```
diff --git a/src/foundation/sigma-decomposition-subuniverse.lagda.md b/src/foundation/sigma-decomposition-subuniverse.lagda.md
index 846913797f..d1527b0936 100644
--- a/src/foundation/sigma-decomposition-subuniverse.lagda.md
+++ b/src/foundation/sigma-decomposition-subuniverse.lagda.md
@@ -26,7 +26,7 @@ Consider a subuniverse `P` and a type `A` in `P`. A **Σ-decomposition** of `A`
 into types in `P` consists of a type `X` in `P` and a family `Y` of types in `P`
 indexed over `X`, equipped with an equivalence
 
-```md
+```text
   A ≃ Σ X Y.
 ```
 
diff --git a/src/foundation/strongly-extensional-maps.lagda.md b/src/foundation/strongly-extensional-maps.lagda.md
index 113662ac4f..8d3745442e 100644
--- a/src/foundation/strongly-extensional-maps.lagda.md
+++ b/src/foundation/strongly-extensional-maps.lagda.md
@@ -19,7 +19,7 @@ open import foundation-core.universe-levels
 Consider a function `f : A → B` between types equipped with apartness relations.
 Then we say that `f` is **strongly extensional** if
 
-```md
+```text
   f x # f y → x # y
 ```
 
diff --git a/src/foundation/symmetric-operations.lagda.md b/src/foundation/symmetric-operations.lagda.md
index 40fe649119..b58863b504 100644
--- a/src/foundation/symmetric-operations.lagda.md
+++ b/src/foundation/symmetric-operations.lagda.md
@@ -31,7 +31,7 @@ open import univalent-combinatorics.standard-finite-types
 Recall that there is a standard unordered pairing operation
 `{-,-} : A → (A → unordered-pair A)`. This induces for any type `B` a map
 
-```md
+```text
   λ f x y → f {x,y} : (unordered-pair A → B) → (A → A → B)
 ```
 
diff --git a/src/foundation/truncation-images-of-maps.lagda.md b/src/foundation/truncation-images-of-maps.lagda.md
index a93750bd63..2639f19068 100644
--- a/src/foundation/truncation-images-of-maps.lagda.md
+++ b/src/foundation/truncation-images-of-maps.lagda.md
@@ -24,7 +24,7 @@ The **`k`-truncation image** of a map `f : A → B` is the type `trunc-im k f`
 that fits in the (`k`-connected,`k`-truncated) factorization of `f`. It is
 defined as the type
 
-```md
+```text
   trunc-im k f := Σ (y : B), type-trunc k (fib f y)
 ```
 
diff --git a/src/foundation/type-duality.lagda.md b/src/foundation/type-duality.lagda.md
index bc7c778b40..bb945e3b60 100644
--- a/src/foundation/type-duality.lagda.md
+++ b/src/foundation/type-duality.lagda.md
@@ -40,14 +40,14 @@ open import trees.polynomial-endofunctors
 Given a univalent universe `𝒰`, we can define two closely related functors
 acting on all types. First there is the covariant functor given by
 
-```md
+```text
   P_𝒰(A) := Σ (X : 𝒰), X → A.
 ```
 
 This is a polynomial endofunctor. Second, there is the contravariant functor
 given by
 
-```md
+```text
   P^𝒰(A) := A → 𝒰.
 ```
 
diff --git a/src/foundation/univalent-type-families.lagda.md b/src/foundation/univalent-type-families.lagda.md
index 36f7051c84..095e1740dc 100644
--- a/src/foundation/univalent-type-families.lagda.md
+++ b/src/foundation/univalent-type-families.lagda.md
@@ -19,7 +19,7 @@ open import foundation-core.universe-levels
 
 A type family `B` over `A` is said to be univalent if the map
 
-```md
+```text
   equiv-tr : (Id x y) → (B x ≃ B y)
 ```
 
diff --git a/src/foundation/universal-property-pullbacks.lagda.md b/src/foundation/universal-property-pullbacks.lagda.md
index 06f4d953e7..a8afb1fb5a 100644
--- a/src/foundation/universal-property-pullbacks.lagda.md
+++ b/src/foundation/universal-property-pullbacks.lagda.md
@@ -27,7 +27,7 @@ open import foundation-core.universe-levels
 The universal property of pullbacks describes the optimal way to complete a
 diagram of the form
 
-```md
+```text
          B
          |
          |
@@ -37,7 +37,7 @@ A -----> X
 
 to a square
 
-```md
+```text
 C -----> B
 |        |
 |        |
diff --git a/src/graph-theory/embeddings-directed-graphs.lagda.md b/src/graph-theory/embeddings-directed-graphs.lagda.md
index d4beff8ce2..d280439f96 100644
--- a/src/graph-theory/embeddings-directed-graphs.lagda.md
+++ b/src/graph-theory/embeddings-directed-graphs.lagda.md
@@ -24,7 +24,7 @@ An embedding of directed graphs is a morphism `f : G → H` of directed graphs
 which is an embedding on vertices such that for each pair `(x , y)` of vertices
 in `G` the map
 
-```md
+```text
   edge-hom-Graph G H : edge-Graph G p → edge-Graph H x y
 ```
 
diff --git a/src/graph-theory/embeddings-undirected-graphs.lagda.md b/src/graph-theory/embeddings-undirected-graphs.lagda.md
index 807ac022cf..328b1256e4 100644
--- a/src/graph-theory/embeddings-undirected-graphs.lagda.md
+++ b/src/graph-theory/embeddings-undirected-graphs.lagda.md
@@ -24,7 +24,7 @@ An embedding of undirected graphs is a morphism `f : G → H` of undirected grap
 which is an embedding on vertices such that for each unordered pair `p` of
 vertices in `G` the map
 
-```md
+```text
   edge-hom-Undirected-Graph G H :
     edge-Undirected-Graph G p →
     edge-Undirected-Graph H (unordered-pair-vertices-hom-Undirected-Graph G H f)
diff --git a/src/graph-theory/eulerian-circuits-undirected-graphs.lagda.md b/src/graph-theory/eulerian-circuits-undirected-graphs.lagda.md
index 3a67e1ce7f..1c9033d98d 100644
--- a/src/graph-theory/eulerian-circuits-undirected-graphs.lagda.md
+++ b/src/graph-theory/eulerian-circuits-undirected-graphs.lagda.md
@@ -28,7 +28,7 @@ such that every edge in `G` is in the image of `T`. In other words, an Eulerian
 circuit `T` consists of `k`-gon `H` equipped with a graph homomorphism
 `f : H → G` that induces an equivalence
 
-```md
+```text
   Σ (unordered-pair-vertices-Polygon k H) (edge-Polygon k H) ≃
   Σ (unordered-pair-vertices-Undirected-Graph G) (edge-Undirected-Graph G)
 ```
diff --git a/src/graph-theory/faithful-morphisms-undirected-graphs.lagda.md b/src/graph-theory/faithful-morphisms-undirected-graphs.lagda.md
index ecddf6b535..86daf7380d 100644
--- a/src/graph-theory/faithful-morphisms-undirected-graphs.lagda.md
+++ b/src/graph-theory/faithful-morphisms-undirected-graphs.lagda.md
@@ -23,7 +23,7 @@ open import graph-theory.undirected-graphs
 A faithful morphism of undirected graphs is a morphism `f : G → H` of undirected
 graphs such that for each unordered pair `p` of vertices in `G` the map
 
-```md
+```text
   edge-hom-Undirected-Graph G H f p :
     edge-Undirected-Graph G p →
     edge-Undirected-Graph H
diff --git a/src/graph-theory/reflecting-maps-undirected-graphs.lagda.md b/src/graph-theory/reflecting-maps-undirected-graphs.lagda.md
index 8e555755fe..78212d3ae4 100644
--- a/src/graph-theory/reflecting-maps-undirected-graphs.lagda.md
+++ b/src/graph-theory/reflecting-maps-undirected-graphs.lagda.md
@@ -24,7 +24,7 @@ open import graph-theory.undirected-graphs
 A reflecting map from an undirected graph `(V , E)` into a type `X` consists of
 a map `fV : V → X` and a map
 
-```md
+```text
   fE : (v : unordered-pair V) → E v → symmetric-Id (map-unordered-pair fV v).
 ```
 
diff --git a/src/group-theory/free-groups-with-one-generator.lagda.md b/src/group-theory/free-groups-with-one-generator.lagda.md
index cb2f1f6b27..c3e5348ba5 100644
--- a/src/group-theory/free-groups-with-one-generator.lagda.md
+++ b/src/group-theory/free-groups-with-one-generator.lagda.md
@@ -36,7 +36,7 @@ open import structured-types.initial-pointed-type-equipped-with-automorphism
 A group `F` equipped with an element `x : F` is said to satisfy the universal
 property of the free group with one generator if for every group `G` the map
 
-```md
+```text
   type-hom-Group F G → type-Group G
 ```
 
diff --git a/src/group-theory/groups.lagda.md b/src/group-theory/groups.lagda.md
index 5b1acda5e2..87898f2377 100644
--- a/src/group-theory/groups.lagda.md
+++ b/src/group-theory/groups.lagda.md
@@ -43,7 +43,7 @@ An **abstract group** is a group in the usual algebraic sense, i.e., it consists
 of a set equipped with a unit element `e`, a binary operation `x, y ↦ xy`, and
 an inverse operation `x ↦ x⁻¹` satisfying the group laws
 
-```md
+```text
   (xy)z = x(yz)      (associativity)
      ex = x          (left unit law)
      xe = x          (right unit law)
diff --git a/src/group-theory/large-semigroups.lagda.md b/src/group-theory/large-semigroups.lagda.md
index 3fb9bf66cf..52a3da5e6c 100644
--- a/src/group-theory/large-semigroups.lagda.md
+++ b/src/group-theory/large-semigroups.lagda.md
@@ -24,7 +24,7 @@ consists of:
   `μ l1 l2 : X l1 → X l2 → X (l1 ⊔ l2)` satisfying the following associativity
   law:
 
-```md
+```text
   μ (l1 ⊔ l2) l3 (μ l1 l2 x y) z ＝ μ l1 (l2 ⊔ l3) x (μ l2 l3 y z).
 ```
 
diff --git a/src/group-theory/normal-submonoids-commutative-monoids.lagda.md b/src/group-theory/normal-submonoids-commutative-monoids.lagda.md
index 0d35702277..4780000efb 100644
--- a/src/group-theory/normal-submonoids-commutative-monoids.lagda.md
+++ b/src/group-theory/normal-submonoids-commutative-monoids.lagda.md
@@ -39,7 +39,7 @@ corresponds uniquely to a saturated congruence relation `~` on `M` consisting of
 the elements congruent to `1`. This is the case if and only if for all `x : M`
 and `u : N` we have
 
-```md
+```text
   xu ∈ N → x ∈ N
 ```
 
diff --git a/src/group-theory/normal-submonoids.lagda.md b/src/group-theory/normal-submonoids.lagda.md
index 685fe2d341..d0d68cfe5d 100644
--- a/src/group-theory/normal-submonoids.lagda.md
+++ b/src/group-theory/normal-submonoids.lagda.md
@@ -43,7 +43,7 @@ relations.
 A submonoid `N` of `M` is normal if and only if for all `x y : M` and `u : N` we
 have
 
-```md
+```text
   xuy ∈ N ⇔ xy ∈ N.
 ```
 
diff --git a/src/group-theory/orbit-stabilizer-theorem-concrete-groups.lagda.md b/src/group-theory/orbit-stabilizer-theorem-concrete-groups.lagda.md
index 1a2aa9bafe..d9cc6ffa5b 100644
--- a/src/group-theory/orbit-stabilizer-theorem-concrete-groups.lagda.md
+++ b/src/group-theory/orbit-stabilizer-theorem-concrete-groups.lagda.md
@@ -26,7 +26,7 @@ The orbit stabilizer theorem for concrete groups asserts that the type
 `Orbit(x)` of orbits of an element `x : X *` is deloopable and fits in a fiber
 sequence
 
-```md
+```text
   BG_x ----> BG ----> B(Orbit(x))
 ```
 
@@ -34,7 +34,7 @@ To see that this is indeed a formulation of the orbit-stabilizer theorem, note
 that the delooping of `Orbit(x)` gives `Orbit(x)` the structure of a group.
 Furthermore, this fiber sequence induces a short exact sequence
 
-```md
+```text
   G_x ----> G ----> Orbit(x),
 ```
 
diff --git a/src/online-encyclopedia-of-integer-sequences/oeis.lagda.md b/src/online-encyclopedia-of-integer-sequences/oeis.lagda.md
index e7e4f0aa44..661ee14d22 100644
--- a/src/online-encyclopedia-of-integer-sequences/oeis.lagda.md
+++ b/src/online-encyclopedia-of-integer-sequences/oeis.lagda.md
@@ -9,6 +9,7 @@ module online-encyclopedia-of-integer-sequences.oeis where
 ```agda
 open import elementary-number-theory.ackermann-function
 open import elementary-number-theory.cofibonacci
+open import elementary-number-theory.collatz-bijection
 open import elementary-number-theory.eulers-totient-function
 open import elementary-number-theory.exponentiation-natural-numbers
 open import elementary-number-theory.factorials
@@ -62,7 +63,7 @@ A000045 : ℕ → ℕ
 A000045 = Fibonacci-ℕ
 ```
 
-### [A000079](https://oeis.org/A000079) Powers of `2
+### [A000079](https://oeis.org/A000079) Powers of `2`
 
 ```agda
 A000079 : ℕ → ℕ
@@ -111,7 +112,14 @@ A001477 : ℕ → ℕ
 A001477 = id
 ```
 
-### [A046859](https://oeis.org/A046859) The main diagonal of the Ackermann-Péter function
+### [A006369](https://oeis.org/A006369) Collatz' bijection
+
+```agda
+A006369 : ℕ → ℕ
+A006369 = map-collatz-bijection
+```
+
+### [A046859](https://oeis.org/A046859) The main diagonal of the Ackermann–Péter function
 
 ```agda
 A046859 : ℕ → ℕ
diff --git a/src/order-theory/frames.lagda.md b/src/order-theory/frames.lagda.md
index 3facd6069a..f1ea1ecc45 100644
--- a/src/order-theory/frames.lagda.md
+++ b/src/order-theory/frames.lagda.md
@@ -30,7 +30,7 @@ arbitrary joins in which meets distribute over suprema. The **distributive law
 for meets over suprema** states that in any
 [meet-suplattice](order-theory.meet-suplattices.md) `A`, we have
 
-```md
+```text
   x ∧ (⋁ᵢ yᵢ) ＝ ⋁ᵢ (x ∧ yᵢ)
 ```
 
diff --git a/src/order-theory/galois-connections-large-posets.lagda.md b/src/order-theory/galois-connections-large-posets.lagda.md
index 6dd9b8739c..29406456c7 100644
--- a/src/order-theory/galois-connections-large-posets.lagda.md
+++ b/src/order-theory/galois-connections-large-posets.lagda.md
@@ -25,7 +25,7 @@ and `Q` consists of
 `f : hom-Large-Poset id P Q` and `hom-Large-Poset id Q P` such that the adjoint
 relation
 
-```md
+```text
   (f x ≤ y) ↔ (x ≤ g y)
 ```
 
diff --git a/src/order-theory/galois-connections.lagda.md b/src/order-theory/galois-connections.lagda.md
index 34c9b69b02..a7c3155706 100644
--- a/src/order-theory/galois-connections.lagda.md
+++ b/src/order-theory/galois-connections.lagda.md
@@ -27,7 +27,7 @@ open import order-theory.posets
 A **Galois connection** between posets `P` and `Q` is a pair of order preserving
 maps `f : P → Q` and `g : Q → P` such that the logical equivalence
 
-```md
+```text
   (f x ≤ y) ↔ (x ≤ g y)
 ```
 
diff --git a/src/order-theory/greatest-lower-bounds-large-posets.lagda.md b/src/order-theory/greatest-lower-bounds-large-posets.lagda.md
index 458eed660e..77a2beb1cc 100644
--- a/src/order-theory/greatest-lower-bounds-large-posets.lagda.md
+++ b/src/order-theory/greatest-lower-bounds-large-posets.lagda.md
@@ -23,7 +23,7 @@ A **greatest binary lower bound** of two elements `a` and `b` in a large poset
 `P` is an element `x` such that for every element `y` in `P` the logical
 equivalence
 
-```md
+```text
   is-binary-lower-bound-Large-Poset P a b y ↔ y ≤ x
 ```
 
diff --git a/src/order-theory/greatest-lower-bounds-posets.lagda.md b/src/order-theory/greatest-lower-bounds-posets.lagda.md
index 7842ac4761..2b2b97638b 100644
--- a/src/order-theory/greatest-lower-bounds-posets.lagda.md
+++ b/src/order-theory/greatest-lower-bounds-posets.lagda.md
@@ -25,7 +25,7 @@ open import order-theory.posets
 A **greatest lower bound** of `a` and `b` in a poset `P` is an element `x` such
 that the logical equivalence
 
-```md
+```text
   ((y ≤ a) ∧ (y ≤ b)) ⇔ (y ≤ x)
 ```
 
@@ -33,7 +33,7 @@ holds for every element `y` in `P`. Similarly, a **greatest lower bound** of a
 family `a : I → P` of elements of `P` is an element `x` of `P` such that the
 logical equivalence
 
-```md
+```text
   (∀ᵢ (y ≤ aᵢ)) ⇔ (y ≤ x)
 ```
 
diff --git a/src/order-theory/large-subposets.lagda.md b/src/order-theory/large-subposets.lagda.md
index 787964d40b..2c7ee670ec 100644
--- a/src/order-theory/large-subposets.lagda.md
+++ b/src/order-theory/large-subposets.lagda.md
@@ -26,7 +26,7 @@ A **large subposet** of a [large poset](order-theory.large-posets.md) `P`
 consists of a subtype `S : type-Large-Poset P l1 → Prop (γ l1)` for each
 universe level `l1` such that the implication
 
-```md
+```text
   ((x ≤ y) ∧ (y ≤ x)) → (x ∈ S → y ∈ S)
 ```
 
diff --git a/src/order-theory/large-subpreorders.lagda.md b/src/order-theory/large-subpreorders.lagda.md
index 38161c5d87..1828a07fcf 100644
--- a/src/order-theory/large-subpreorders.lagda.md
+++ b/src/order-theory/large-subpreorders.lagda.md
@@ -22,7 +22,7 @@ open import order-theory.large-preorders
 A **large subpreorder** of a [large preorder](order-theory.large-preorders.md)
 `P` consists of a subtype
 
-```md
+```text
   S : type-Large-Preorder P l → Prop (γ l)
 ```
 
diff --git a/src/order-theory/large-suplattices.lagda.md b/src/order-theory/large-suplattices.lagda.md
index 18fa892097..25867ef371 100644
--- a/src/order-theory/large-suplattices.lagda.md
+++ b/src/order-theory/large-suplattices.lagda.md
@@ -25,14 +25,14 @@ open import order-theory.upper-bounds-large-posets
 A **large suplattice** is a [large poset](order-theory.large-posets.md) `P` such
 that for every family
 
-```md
+```text
   x : I → type-Large-Poset P l1
 ```
 
 indexed by `I : UU l2` there is an element `⋁ x : type-Large-Poset P (l1 ⊔ l2)`
 such that the logical equivalence
 
-```md
+```text
   (∀ᵢ xᵢ ≤ y) ↔ ((⋁ x) ≤ y)
 ```
 
diff --git a/src/order-theory/least-upper-bounds-large-posets.lagda.md b/src/order-theory/least-upper-bounds-large-posets.lagda.md
index a7cf7c6a47..a53e001394 100644
--- a/src/order-theory/least-upper-bounds-large-posets.lagda.md
+++ b/src/order-theory/least-upper-bounds-large-posets.lagda.md
@@ -22,7 +22,7 @@ open import order-theory.upper-bounds-large-posets
 A **least upper bound** of a family of elements `a : I → P` in a large poset `P`
 is an element `x` in `P` such that the logial equivalence
 
-```md
+```text
   is-upper-bound-family-of-elements-Large-Poset P a y ↔ (x ≤ y)
 ```
 
diff --git a/src/order-theory/least-upper-bounds-posets.lagda.md b/src/order-theory/least-upper-bounds-posets.lagda.md
index b2393f0244..274aa0eca0 100644
--- a/src/order-theory/least-upper-bounds-posets.lagda.md
+++ b/src/order-theory/least-upper-bounds-posets.lagda.md
@@ -25,7 +25,7 @@ open import order-theory.upper-bounds-posets
 A **least upper bound** of `a` and `b` in a poset `P` is an element `x` such
 that the logical equivalence
 
-```md
+```text
   ((a ≤ y) ∧ (b ≤ y)) ⇔ (x ≤ y)
 ```
 
@@ -33,7 +33,7 @@ holds for every element `y` in `P`. Similarly, a **least upper bound** of a
 family `a : I → P` of elements of `P` is an element `x` of `P` such that the
 logical equivalence
 
-```md
+```text
   (∀ᵢ (aᵢ ≤ y)) ⇔ (x ≤ y)
 ```
 
diff --git a/src/order-theory/order-preserving-maps-large-posets.lagda.md b/src/order-theory/order-preserving-maps-large-posets.lagda.md
index eae2d7dd4a..77a3f65076 100644
--- a/src/order-theory/order-preserving-maps-large-posets.lagda.md
+++ b/src/order-theory/order-preserving-maps-large-posets.lagda.md
@@ -19,7 +19,7 @@ open import order-theory.order-preserving-maps-large-preorders
 
 An order preserving map between large posets from `P` to `Q` consists of a map
 
-```md
+```text
   f : type-Large-Poset P l1 → type-Large-Poset Q (γ l1)
 ```
 
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 d61537f5d9..2f27a3f10d 100644
--- a/src/order-theory/order-preserving-maps-large-preorders.lagda.md
+++ b/src/order-theory/order-preserving-maps-large-preorders.lagda.md
@@ -19,7 +19,7 @@ open import order-theory.large-preorders
 An order preserving map between large preorders from `P` to `Q` consists of a
 map
 
-```md
+```text
   f : type-Large-Preorder P l1 → type-Large-Preorder Q (γ l1)
 ```
 
diff --git a/src/order-theory/posets.lagda.md b/src/order-theory/posets.lagda.md
index f1e8934093..8d6a5780b9 100644
--- a/src/order-theory/posets.lagda.md
+++ b/src/order-theory/posets.lagda.md
@@ -101,7 +101,7 @@ module _
 
 Inequalities in preorders can be constructed by equational reasoning as follows:
 
-```md
+```text
 calculate-in-Poset X
   chain-of-inequalities
   x ≤ y
diff --git a/src/order-theory/preorders.lagda.md b/src/order-theory/preorders.lagda.md
index c1d2f7c91e..fba1611606 100644
--- a/src/order-theory/preorders.lagda.md
+++ b/src/order-theory/preorders.lagda.md
@@ -85,7 +85,7 @@ module _
 
 Inequalities in preorders can be constructed by equational reasoning as follows:
 
-```md
+```text
 calculate-in-Preorder X
   chain-of-inequalities
   x ≤ y
diff --git a/src/orthogonal-factorization-systems/extensions-of-maps.lagda.md b/src/orthogonal-factorization-systems/extensions-of-maps.lagda.md
index ee5a9543a8..ce0df4d662 100644
--- a/src/orthogonal-factorization-systems/extensions-of-maps.lagda.md
+++ b/src/orthogonal-factorization-systems/extensions-of-maps.lagda.md
@@ -40,7 +40,7 @@ An _extension_ of a map `f : (x : A) → P x` along a map `i : A → B` is a map
 `g : (y : B) → Q y` such that `Q` restricts along `i` to `P` and `g` restricts
 along `i` to `f`.
 
-```md
+```text
   A
   |  \
   i    f
@@ -92,7 +92,7 @@ module _
 
 ### Vertical composition of extensions of maps
 
-```md
+```text
   A
   |  \
   i    f
@@ -120,7 +120,7 @@ module _
 
 ### Horizontal composition of extensions of maps
 
-```md
+```text
            A
         /  |  \
       f    g    h
@@ -160,7 +160,7 @@ module _
 
 ### Left whiskering of extensions of maps
 
-```md
+```text
   A
   |  \
   i    f
@@ -183,7 +183,7 @@ module _
 
 ### Right whiskering of extensions of maps
 
-```md
+```text
   X - h -> A
            |  \
            i    f
diff --git a/src/orthogonal-factorization-systems/factorization-operations-function-classes.lagda.md b/src/orthogonal-factorization-systems/factorization-operations-function-classes.lagda.md
index d52df4f408..13cbd34753 100644
--- a/src/orthogonal-factorization-systems/factorization-operations-function-classes.lagda.md
+++ b/src/orthogonal-factorization-systems/factorization-operations-function-classes.lagda.md
@@ -25,7 +25,7 @@ A **factorization operation into function classes** is a factorization operation
 equipped with two function classes `L` and `R` such that the left map of every
 factorization is in `L`, and the right map is in `R`.
 
-```md
+```text
        ∙
       ^ \
  L ∋ /   \ ∈ R
diff --git a/src/orthogonal-factorization-systems/factorization-operations.lagda.md b/src/orthogonal-factorization-systems/factorization-operations.lagda.md
index 710396fcda..a30bcdf8d8 100644
--- a/src/orthogonal-factorization-systems/factorization-operations.lagda.md
+++ b/src/orthogonal-factorization-systems/factorization-operations.lagda.md
@@ -19,7 +19,7 @@ open import orthogonal-factorization-systems.factorizations-of-maps
 A **factorization operation** on a function type `A → B` is a choice of
 factorization for every map `f` in `A → B`.
 
-```md
+```text
        ∙
       ^ \
      /   \
diff --git a/src/orthogonal-factorization-systems/factorizations-of-maps.lagda.md b/src/orthogonal-factorization-systems/factorizations-of-maps.lagda.md
index b5c5d5c00d..2412d4e5c4 100644
--- a/src/orthogonal-factorization-systems/factorizations-of-maps.lagda.md
+++ b/src/orthogonal-factorization-systems/factorizations-of-maps.lagda.md
@@ -29,7 +29,7 @@ open import orthogonal-factorization-systems.function-classes
 A **factorization** of a map `f : A → B` is a pair of maps `g : X → B` and
 `h : A → X` such that their composite `g ∘ h` is `f`.
 
-```md
+```text
        X
       ^ \
    h /   \ g
diff --git a/src/orthogonal-factorization-systems/lifting-operations.lagda.md b/src/orthogonal-factorization-systems/lifting-operations.lagda.md
index 46eb0fb30a..3e2f41c74c 100644
--- a/src/orthogonal-factorization-systems/lifting-operations.lagda.md
+++ b/src/orthogonal-factorization-systems/lifting-operations.lagda.md
@@ -23,7 +23,7 @@ open import orthogonal-factorization-systems.pullback-hom
 Given two maps, `f : A → X` and `g : B → Y`, a _lifting operation between `f`
 and `g`_ is a choice of lifting square for every commuting square
 
-```md
+```text
   A ------> B
   |         |
  f|         |g
diff --git a/src/orthogonal-factorization-systems/lifting-squares.lagda.md b/src/orthogonal-factorization-systems/lifting-squares.lagda.md
index 27faf6dee4..b4a71af441 100644
--- a/src/orthogonal-factorization-systems/lifting-squares.lagda.md
+++ b/src/orthogonal-factorization-systems/lifting-squares.lagda.md
@@ -25,7 +25,7 @@ open import orthogonal-factorization-systems.lifts-of-maps
 
 A _lifting square_ is a commuting square
 
-```md
+```text
        h
   A ------> B
   |         |
@@ -38,7 +38,7 @@ A _lifting square_ is a commuting square
 
 together with a diagonal map `j : X → B` such that the complete diagram
 
-```md
+```text
        h
   A ------> B
   |       ^ |
@@ -175,7 +175,7 @@ module _
 
 The diagram
 
-```md
+```text
   A         B
   |       ^ |
  f|   j  /  |g
@@ -186,7 +186,7 @@ The diagram
 
 gives rise to a lifting square
 
-```md
+```text
      j ∘ f
   A ------> B
   |       ^ |
diff --git a/src/orthogonal-factorization-systems/lifts-of-maps.lagda.md b/src/orthogonal-factorization-systems/lifts-of-maps.lagda.md
index a158d02cee..b7a9f51f1b 100644
--- a/src/orthogonal-factorization-systems/lifts-of-maps.lagda.md
+++ b/src/orthogonal-factorization-systems/lifts-of-maps.lagda.md
@@ -31,7 +31,7 @@ open import foundation.universe-levels
 A _lift_ of a map `f : X → B` along a map `i : A → B` is a map `g : X → A` such
 that the composition `i ∘ g` is `f`.
 
-```md
+```text
            A
           ^|
         /  i
@@ -72,7 +72,7 @@ module _
 
 ### Vertical composition of lifts of maps
 
-```md
+```text
            A
           ^|
         /  i
@@ -98,7 +98,7 @@ module _
 
 ### Horizontal composition of lifts of maps
 
-```md
+```text
   A - f -> B - g -> C
     \      |      /
       h    i    j
@@ -120,7 +120,7 @@ module _
 
 ## Left whiskering of lifts of maps
 
-```md
+```text
            A
           ^|
         /  i
@@ -141,7 +141,7 @@ module _
 
 ## Right whiskering of lifts of maps
 
-```md
+```text
                     A
                    ^|
                  /  i
diff --git a/src/orthogonal-factorization-systems/local-types.lagda.md b/src/orthogonal-factorization-systems/local-types.lagda.md
index 8d4efc8c14..bd8d3819d2 100644
--- a/src/orthogonal-factorization-systems/local-types.lagda.md
+++ b/src/orthogonal-factorization-systems/local-types.lagda.md
@@ -34,7 +34,7 @@ open import foundation-core.universe-levels
 A type family `A` over `X` is said to be **local at** `f : Y → X`, or
 **`f`-local**, if the precomposition map
 
-```md
+```text
   _∘ f : ((x : X) → A x) → ((y : Y) → A (f y))
 ```
 
diff --git a/src/orthogonal-factorization-systems/null-types.lagda.md b/src/orthogonal-factorization-systems/null-types.lagda.md
index dba97a3c26..16b50d0ff5 100644
--- a/src/orthogonal-factorization-systems/null-types.lagda.md
+++ b/src/orthogonal-factorization-systems/null-types.lagda.md
@@ -24,7 +24,7 @@ open import orthogonal-factorization-systems.local-types
 
 A type `A` is said to be **null at** `Y`, or **`Y`-null**, if the constant map
 
-```md
+```text
   const : A → (Y → A)
 ```
 
diff --git a/src/orthogonal-factorization-systems/pullback-hom.lagda.md b/src/orthogonal-factorization-systems/pullback-hom.lagda.md
index eddb3a981b..bdaba988d7 100644
--- a/src/orthogonal-factorization-systems/pullback-hom.lagda.md
+++ b/src/orthogonal-factorization-systems/pullback-hom.lagda.md
@@ -24,27 +24,27 @@ open import foundation.universe-levels
 
 ## Idea
 
-Given a pair of maps `f : A → X` and `g : B → Y`, there is a commuting square
+Given a pair of maps `f : A → B` and `g : X → Y`, there is a commuting square
 
-```md
+```text
           - ∘ f
-    B → X ----> B → A
-      |            |
-g ∘ - |            | g ∘ -
-      V            V
-    Y → X ----> Y → A.
+    B → X ----> A → X
+      |           |
+g ∘ - |           | g ∘ -
+      V           V
+    B → Y ----> A → Y.
           - ∘ f
 ```
 
 The **pullback-hom** of `f` and `g` is the comparison map from `B → X` to the
 pullback of the cospan:
 
-```md
-      ∙ -------> B → A
-      |  ⌟         |
-      |            | g ∘ -
-      V            V
-    Y → X ----> Y → A.
+```text
+      ∙ ------> A → X
+      |  ⌟        |
+      |           | g ∘ -
+      V           V
+    B → Y ----> A → Y.
           - ∘ f
 ```
 
@@ -56,7 +56,7 @@ from `f` to `g`, i.e. commuting squares where the vertical maps are `f` and `g`.
 ```agda
 module _
   {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
-  (f : A → X) (g : B → Y)
+  (f : A → B) (g : X → Y)
   where
 
   type-pullback-hom : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
@@ -73,14 +73,14 @@ module _
 
 ### The pullback-hom map
 
-The pullback-hom is the canonical gap map `(X → B) → type-pullback-hom` and can
+The pullback-hom is the canonical gap map `(B → X) → type-pullback-hom` and can
 be interpreted as the map that takes a diagonal map `j` from the codomain of `f`
 to the domain of `g` to the fibered map `((g ∘ j) , (j ∘ f) , refl-htpy)`.
 
 ```agda
-  pullback-hom : (X → B) → type-pullback-hom
+  pullback-hom : (B → X) → type-pullback-hom
   pullback-hom =
-    gap-pullback-hom (postcomp X g , precomp f B , refl-htpy)
+    gap-pullback-hom (postcomp B g , precomp f X , refl-htpy)
 ```
 
 ## Properties
@@ -91,10 +91,10 @@ to the domain of `g` to the fibered map `((g ∘ j) , (j ∘ f) , refl-htpy)`.
 module _
   {l1 l2 l3 l4 : Level}
   {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
-  (f : A → X) (g : B → Y)
+  (f : A → B) (g : X → Y)
   {l1' l2' l3' l4' : Level}
   {A' : UU l1'} {B' : UU l2'} {X' : UU l3'} {Y' : UU l4'}
-  (f' : A' → X') (g' : B' → Y')
+  (f' : A' → B') (g' : X' → Y')
   where
 
   map-pullback-hom :
@@ -113,7 +113,7 @@ module _
 ```agda
 module _
   {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
-  (f : A → X) (g : B → Y)
+  (f : A → B) (g : X → Y)
   where
 
   equiv-fibered-map-type-pullback-hom :
diff --git a/src/ring-theory/algebras-rings.lagda.md b/src/ring-theory/algebras-rings.lagda.md
index 128b5960a9..efb0acae84 100644
--- a/src/ring-theory/algebras-rings.lagda.md
+++ b/src/ring-theory/algebras-rings.lagda.md
@@ -23,7 +23,7 @@ open import ring-theory.rings
 An algebra over a ring `R` consists of an `R`-module `M` equipped with a binary
 operation `x y ↦ xy : M → M → M` such that
 
-```md
+```text
   (xy)z  = x(yz)
   r(xy)  = (rx)y
   r(xy)  = x(ry)
diff --git a/src/ring-theory/binomial-theorem-rings.lagda.md b/src/ring-theory/binomial-theorem-rings.lagda.md
index ac98270a33..6fe691d44f 100644
--- a/src/ring-theory/binomial-theorem-rings.lagda.md
+++ b/src/ring-theory/binomial-theorem-rings.lagda.md
@@ -34,7 +34,7 @@ The binomial theorem for rings asserts that for any two elements `x` and `y` of
 a commutative ring `R` and any natural number `n`, if `xy ＝ yx` holds then we
 have
 
-```md
+```text
   (x + y)ⁿ = ∑_{0 ≤ i < n+1} (n choose i) xⁱ yⁿ⁻ⁱ.
 ```
 
diff --git a/src/ring-theory/binomial-theorem-semirings.lagda.md b/src/ring-theory/binomial-theorem-semirings.lagda.md
index fdaf7c6033..bf84354799 100644
--- a/src/ring-theory/binomial-theorem-semirings.lagda.md
+++ b/src/ring-theory/binomial-theorem-semirings.lagda.md
@@ -35,7 +35,7 @@ The binomial theorem in semirings asserts that for any two elements `x` and `y`
 of a commutative ring `R` and any natural number `n`, if `xy = yx` holds then we
 have
 
-```md
+```text
   (x + y)ⁿ = ∑_{0 ≤ i < n+1} (n choose i) xⁱ yⁿ⁻ⁱ.
 ```
 
diff --git a/src/ring-theory/modules-rings.lagda.md b/src/ring-theory/modules-rings.lagda.md
index a6010cb9e2..5e06f68aba 100644
--- a/src/ring-theory/modules-rings.lagda.md
+++ b/src/ring-theory/modules-rings.lagda.md
@@ -29,7 +29,7 @@ open import ring-theory.rings
 A (left) module `M` over a ring `R` consists of an abelian group `M` equipped
 with an action `R → M → M` such
 
-```md
+```text
   r(x+y) = rx + ry
       r0 = 0
    r(-x) = -(rx)
diff --git a/src/species/cauchy-composition-species-of-types-in-subuniverses.lagda.md b/src/species/cauchy-composition-species-of-types-in-subuniverses.lagda.md
index 92f1e47c28..5aadeaec40 100644
--- a/src/species/cauchy-composition-species-of-types-in-subuniverses.lagda.md
+++ b/src/species/cauchy-composition-species-of-types-in-subuniverses.lagda.md
@@ -42,7 +42,7 @@ open import species.unit-cauchy-composition-species-of-types-in-subuniverses
 A species `S : type-subuniverse P → type-subuniverse Q` induces its
 [Cauchy series](species.cauchy-series-species-of-types-in-subuniverses.md)
 
-```md
+```text
   X ↦ Σ (A : type-subuniverse P), (S A) × (A → X)
 ```
 
diff --git a/src/species/cauchy-composition-species-of-types.lagda.md b/src/species/cauchy-composition-species-of-types.lagda.md
index 417383e082..d007ea24c2 100644
--- a/src/species/cauchy-composition-species-of-types.lagda.md
+++ b/src/species/cauchy-composition-species-of-types.lagda.md
@@ -39,7 +39,7 @@ open import species.unit-cauchy-composition-species-of-types
 A species of types `S : UU l1 → UU l2` can be thought of as the polynomial
 endofunctor
 
-```md
+```text
   X ↦ Σ (A : UU l1) (S A) × (A → X)
 ```
 
diff --git a/src/species/cauchy-exponentials-species-of-types-in-subuniverses.lagda.md b/src/species/cauchy-exponentials-species-of-types-in-subuniverses.lagda.md
index 22b4b22fa7..d6af23c2ae 100644
--- a/src/species/cauchy-exponentials-species-of-types-in-subuniverses.lagda.md
+++ b/src/species/cauchy-exponentials-species-of-types-in-subuniverses.lagda.md
@@ -42,7 +42,7 @@ open import species.species-of-types-in-subuniverses
 The **Cauchy exponential** of a species `S : P → Q` of types in subuniverse is
 defined by
 
-```md
+```text
   X ↦ Σ ((U , V , e) : Σ-Decomposition-subuniverse P X),  Π (u : U) → S (V u).
 ```
 
diff --git a/src/species/cauchy-exponentials-species-of-types.lagda.md b/src/species/cauchy-exponentials-species-of-types.lagda.md
index d3dda562c6..5294ecf6ba 100644
--- a/src/species/cauchy-exponentials-species-of-types.lagda.md
+++ b/src/species/cauchy-exponentials-species-of-types.lagda.md
@@ -41,7 +41,7 @@ Cauchy composite `exp ∘ S`. Since the exponent species is defined as `X ↦ 
 the coefficients of the Cauchy exponential of `S` are defined as follows:
 species of types :
 
-```md
+```text
   X ↦ Σ ((U , V , e) : Relaxed-Σ-Decomposition X),  Π (u : U) → S (V u).
 ```
 
diff --git a/src/species/cauchy-products-species-of-types-in-subuniverses.lagda.md b/src/species/cauchy-products-species-of-types-in-subuniverses.lagda.md
index f217c5e01f..9b55af65b9 100644
--- a/src/species/cauchy-products-species-of-types-in-subuniverses.lagda.md
+++ b/src/species/cauchy-products-species-of-types-in-subuniverses.lagda.md
@@ -37,7 +37,7 @@ open import species.species-of-types-in-subuniverses
 The **Cauchy product** of two species `S` and `T` from `P` to `Q` of types in a
 subuniverse is defined by
 
-```md
+```text
   X ↦ Σ (k : P), Σ (k' : P), Σ (e : k + k' ≃ X), S(k) × T(k')
 ```
 
diff --git a/src/species/cauchy-products-species-of-types.lagda.md b/src/species/cauchy-products-species-of-types.lagda.md
index 8f499da9b2..1d4560f78f 100644
--- a/src/species/cauchy-products-species-of-types.lagda.md
+++ b/src/species/cauchy-products-species-of-types.lagda.md
@@ -21,7 +21,7 @@ open import species.species-of-types
 
 The Cauchy product of two species of types `S` and `T` on `X` is defined as
 
-```md
+```text
   Σ (k : UU) (Σ (k' : UU) (Σ (e : k + k' ≃ X) S(k) × T(k')))
 ```
 
diff --git a/src/species/cauchy-series-species-of-types-in-subuniverses.lagda.md b/src/species/cauchy-series-species-of-types-in-subuniverses.lagda.md
index ca3a86d1c8..1ebcaedc43 100644
--- a/src/species/cauchy-series-species-of-types-in-subuniverses.lagda.md
+++ b/src/species/cauchy-series-species-of-types-in-subuniverses.lagda.md
@@ -30,7 +30,7 @@ open import species.species-of-types-in-subuniverses
 The **Cauchy series** of a species `S` of types in subuniverse from `P` to `Q`
 at `X` is defined as :
 
-```md
+```text
 Σ (U : type-subuniverse P) (S(U) × (U → X))
 ```
 
diff --git a/src/species/cauchy-series-species-of-types.lagda.md b/src/species/cauchy-series-species-of-types.lagda.md
index e6369f4526..0e812eed03 100644
--- a/src/species/cauchy-series-species-of-types.lagda.md
+++ b/src/species/cauchy-series-species-of-types.lagda.md
@@ -25,20 +25,20 @@ open import species.species-of-types
 In classical mathematics, the Cauchy series of a species (of finite types) `S`
 is the formal series in `x` :
 
-```md
+```text
 Σ (n : ℕ) (|S({1,...,n}| x^n / n!))
 ```
 
 The categorified version of this series is :
 
-```md
+```text
   Σ (F : 𝔽), S(F) × (F → X)
 ```
 
 Remarks that we can generalized this to species of types with the following
 definition :
 
-```md
+```text
   Σ (U : UU), S(U) × (U → X)
 ```
 
diff --git a/src/species/dirichlet-products-species-of-types-in-subuniverses.lagda.md b/src/species/dirichlet-products-species-of-types-in-subuniverses.lagda.md
index 21448d01a3..74742be2bd 100644
--- a/src/species/dirichlet-products-species-of-types-in-subuniverses.lagda.md
+++ b/src/species/dirichlet-products-species-of-types-in-subuniverses.lagda.md
@@ -31,7 +31,7 @@ open import species.species-of-types-in-subuniverses
 The Dirichlet product of two species of subuniverse `S` and `T` from `P` to `Q`
 on `X` is defined as
 
-```md
+```text
   Σ (k : P) (Σ (k' : P) (Σ (e : k × k' ≃ X) S(k) × T(k')))
 ```
 
diff --git a/src/species/small-cauchy-composition-species-of-types-in-subuniverses.lagda.md b/src/species/small-cauchy-composition-species-of-types-in-subuniverses.lagda.md
index f0f7f699b3..8c09d2189c 100644
--- a/src/species/small-cauchy-composition-species-of-types-in-subuniverses.lagda.md
+++ b/src/species/small-cauchy-composition-species-of-types-in-subuniverses.lagda.md
@@ -40,7 +40,7 @@ open import species.unit-cauchy-composition-species-of-types
 A species `S : Inhabited-Type → UU l` can be thought of as the analytic
 endofunctor
 
-```md
+```text
   X ↦ Σ (A : Inhabited-Type) (S A) × (A → X)
 ```
 
diff --git a/src/species/unit-cauchy-composition-species-of-types-in-subuniverses.lagda.md b/src/species/unit-cauchy-composition-species-of-types-in-subuniverses.lagda.md
index 49bb896046..f986c7f833 100644
--- a/src/species/unit-cauchy-composition-species-of-types-in-subuniverses.lagda.md
+++ b/src/species/unit-cauchy-composition-species-of-types-in-subuniverses.lagda.md
@@ -23,7 +23,7 @@ open import species.species-of-types-in-subuniverses
 Given a global subuniverse closed under `is-contr`, we define the unit of the
 Cauchy composition of species of types in a subuniverse by
 
-```md
+```text
   X ↦ is-contr X.
 ```
 
diff --git a/src/species/unit-cauchy-composition-species-of-types.lagda.md b/src/species/unit-cauchy-composition-species-of-types.lagda.md
index 785b706523..15884d5b45 100644
--- a/src/species/unit-cauchy-composition-species-of-types.lagda.md
+++ b/src/species/unit-cauchy-composition-species-of-types.lagda.md
@@ -19,7 +19,7 @@ open import species.species-of-types
 
 The **unit** of Cauchy composition of species of types is the species
 
-```md
+```text
   X ↦ is-contr X.
 ```
 
diff --git a/src/structured-types/commuting-squares-of-pointed-maps.lagda.md b/src/structured-types/commuting-squares-of-pointed-maps.lagda.md
index 8633e7287b..74c2702ec7 100644
--- a/src/structured-types/commuting-squares-of-pointed-maps.lagda.md
+++ b/src/structured-types/commuting-squares-of-pointed-maps.lagda.md
@@ -20,7 +20,7 @@ open import structured-types.pointed-types
 
 A coherence square of pointed maps
 
-```md
+```text
   A ------> X
   |         |
   |         |
diff --git a/src/structured-types/symmetric-elements-involutive-types.lagda.md b/src/structured-types/symmetric-elements-involutive-types.lagda.md
index 179a332e3a..d9f5ee8705 100644
--- a/src/structured-types/symmetric-elements-involutive-types.lagda.md
+++ b/src/structured-types/symmetric-elements-involutive-types.lagda.md
@@ -22,7 +22,7 @@ Symmetric elements of involutive types are fixed points of the involution. In
 other words, the type of symmetric elements of an involutive type `A` is defined
 to be
 
-```md
+```text
   (X : 2-Element-Type lzero) → A X
 ```
 
diff --git a/src/synthetic-homotopy-theory/cocones-under-spans.lagda.md b/src/synthetic-homotopy-theory/cocones-under-spans.lagda.md
index 95eeb0896e..20b43fc95f 100644
--- a/src/synthetic-homotopy-theory/cocones-under-spans.lagda.md
+++ b/src/synthetic-homotopy-theory/cocones-under-spans.lagda.md
@@ -29,7 +29,7 @@ open import foundation.universe-levels
 A cocone under a span `A <-f- S -g-> B` with vertex `X` consists of two maps
 `i : A → X` and `j : B → X` equipped with a homotopy witnessing that the square
 
-```md
+```text
       g
   S -----> B
   |        |
diff --git a/src/synthetic-homotopy-theory/smash-products-of-pointed-types.lagda.md b/src/synthetic-homotopy-theory/smash-products-of-pointed-types.lagda.md
index 6400a902df..bb96761f19 100644
--- a/src/synthetic-homotopy-theory/smash-products-of-pointed-types.lagda.md
+++ b/src/synthetic-homotopy-theory/smash-products-of-pointed-types.lagda.md
@@ -27,7 +27,7 @@ open import synthetic-homotopy-theory.wedges-of-pointed-types
 Given two pointed types `a : A` and `b : B` we may form their **smash product**
 as the following pushout
 
-```md
+```text
  A ∨∗ B ----> A ×∗ B
     |           |
     |           |
diff --git a/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md b/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md
index d747c8f263..6c5ad6dfe3 100644
--- a/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md
@@ -77,7 +77,7 @@ The universal property of the pushout of a span `S` can also be stated as a
 pullback-property: a cocone `c ≐ pair i (pair j H)` with vertex `X` satisfies
 the universal property of the pushout of `S` if and only if the square
 
-```md
+```text
   Y^X -----> Y^B
    |          |
    |          |
diff --git a/src/synthetic-homotopy-theory/wedges-of-pointed-types.lagda.md b/src/synthetic-homotopy-theory/wedges-of-pointed-types.lagda.md
index b907d0fb51..55e818323a 100644
--- a/src/synthetic-homotopy-theory/wedges-of-pointed-types.lagda.md
+++ b/src/synthetic-homotopy-theory/wedges-of-pointed-types.lagda.md
@@ -29,7 +29,7 @@ open import synthetic-homotopy-theory.pushouts-of-pointed-types
 The **wedge** or **wedge sum** of two pointed types `a : A` and `b : B` is
 defined by the following pushout.
 
-```md
+```text
   unit ------> A
     |          |
     |          |
diff --git a/src/trees/coalgebra-of-directed-trees.lagda.md b/src/trees/coalgebra-of-directed-trees.lagda.md
index cdffe2ed95..e581169de0 100644
--- a/src/trees/coalgebra-of-directed-trees.lagda.md
+++ b/src/trees/coalgebra-of-directed-trees.lagda.md
@@ -24,7 +24,7 @@ Using the fibers of base elements, the type of directed trees, of which the type
 of nodes and the types of edges are of the same universe level, has the
 structure of a coalgebra for the polynomial endofunctor
 
-```md
+```text
   A ↦ Σ (X : UU), X → A
 ```
 
diff --git a/src/trees/coalgebra-of-enriched-directed-trees.lagda.md b/src/trees/coalgebra-of-enriched-directed-trees.lagda.md
index b7ba8263d2..32cae5c137 100644
--- a/src/trees/coalgebra-of-enriched-directed-trees.lagda.md
+++ b/src/trees/coalgebra-of-enriched-directed-trees.lagda.md
@@ -25,7 +25,7 @@ open import trees.polynomial-endofunctors
 Using the fibers of base elements, the type of enriched directed trees has the
 structure of a coalgebra for the polynomial endofunctor
 
-```md
+```text
   X ↦ Σ (a : A), B a → X.
 ```
 
diff --git a/src/trees/coalgebras-polynomial-endofunctors.lagda.md b/src/trees/coalgebras-polynomial-endofunctors.lagda.md
index 8760404de6..85f9f915c3 100644
--- a/src/trees/coalgebras-polynomial-endofunctors.lagda.md
+++ b/src/trees/coalgebras-polynomial-endofunctors.lagda.md
@@ -20,7 +20,7 @@ open import trees.polynomial-endofunctors
 **Coalgebras** for polynomial endofunctors are types `X` equipped with a
 function
 
-```md
+```text
   X → Σ (a : A), B a → X
 ```
 
diff --git a/src/trees/enriched-directed-trees.lagda.md b/src/trees/enriched-directed-trees.lagda.md
index 8fdfc30df1..1c773d083d 100644
--- a/src/trees/enriched-directed-trees.lagda.md
+++ b/src/trees/enriched-directed-trees.lagda.md
@@ -33,13 +33,13 @@ open import trees.directed-trees
 Consider a type `A` and a type family `B` over `A`. An **`(A,B)`-enriched
 directed tree** is a directed tree `T` equipped with a map
 
-```md
+```text
   shape : node-Directed-Tree T → A
 ```
 
 and for each node `x` an equivalence
 
-```md
+```text
   e : B (shape x) ≃ Σ (node-Directed-Tree T) (λ y → edge-Directed-Tree T y x)
 ```
 
diff --git a/src/trees/extensional-w-types.lagda.md b/src/trees/extensional-w-types.lagda.md
index 2b2daddd54..575f72873e 100644
--- a/src/trees/extensional-w-types.lagda.md
+++ b/src/trees/extensional-w-types.lagda.md
@@ -36,7 +36,7 @@ open import trees.w-types
 A W-type `𝕎 A B` is said to be **extensional** if for any two elements
 `S T : 𝕎 A B` the induced map
 
-```md
+```text
   Id S T → ((U : 𝕎 A B) → (U ∈-𝕎 S) ≃ (U ∈-𝕎 T))
 ```
 
diff --git a/src/trees/functoriality-combinator-directed-trees.lagda.md b/src/trees/functoriality-combinator-directed-trees.lagda.md
index 66c9d83f92..4330e0544b 100644
--- a/src/trees/functoriality-combinator-directed-trees.lagda.md
+++ b/src/trees/functoriality-combinator-directed-trees.lagda.md
@@ -29,7 +29,7 @@ open import trees.rooted-morphisms-directed-trees
 Given a family of rooted morphisms `fᵢ : Sᵢ → Tᵢ` of directed trees, we obtain a
 morphism
 
-```md
+```text
   combinator f : combinator S → combinator T
 ```
 
diff --git a/src/trees/indexed-w-types.lagda.md b/src/trees/indexed-w-types.lagda.md
index 081f0e8991..7ac1f06423 100644
--- a/src/trees/indexed-w-types.lagda.md
+++ b/src/trees/indexed-w-types.lagda.md
@@ -18,7 +18,7 @@ open import foundation.universe-levels
 containers. The main idea is that indexed W-types are initial algebras for the
 polynomial endofunctor
 
-```md
+```text
   (X : I → UU) ↦ Σ (a : A i), Π (b : B i a), X (f i a b),
 ```
 
diff --git a/src/trees/morphisms-algebras-polynomial-endofunctors.lagda.md b/src/trees/morphisms-algebras-polynomial-endofunctors.lagda.md
index 8c7a3a6c18..92abe8243d 100644
--- a/src/trees/morphisms-algebras-polynomial-endofunctors.lagda.md
+++ b/src/trees/morphisms-algebras-polynomial-endofunctors.lagda.md
@@ -30,7 +30,7 @@ A **morphism** of algebras of a polynomial endofunctor `P A B` consists of a map
 `f : X → Y$ between the underlying types, equipped with a homotopy witnessing
 that the square
 
-```md
+```text
            P A B f
   P A B X ---------> P A B Y
       |                |
diff --git a/src/trees/morphisms-coalgebras-polynomial-endofunctors.lagda.md b/src/trees/morphisms-coalgebras-polynomial-endofunctors.lagda.md
index 342b17daf3..9e3ce030c9 100644
--- a/src/trees/morphisms-coalgebras-polynomial-endofunctors.lagda.md
+++ b/src/trees/morphisms-coalgebras-polynomial-endofunctors.lagda.md
@@ -30,7 +30,7 @@ A **morphism** of coalgebras of a polynomial endofunctor `P A B` consists of a
 function `f : X → Y` between their underlying types, equipped with a homotopy
 witnessing that the square
 
-```md
+```text
               f
       X -------------> Y
       |                |
diff --git a/src/trees/polynomial-endofunctors.lagda.md b/src/trees/polynomial-endofunctors.lagda.md
index f6b4357462..45ccaefd2e 100644
--- a/src/trees/polynomial-endofunctors.lagda.md
+++ b/src/trees/polynomial-endofunctors.lagda.md
@@ -26,7 +26,7 @@ open import foundation.universe-levels
 Given a type `A` equipped with a type family `B` over `A`, the **polynomial
 endofunctor** `P A B` is defined by
 
-```md
+```text
   X ↦ Σ (x : A), (B x → X)
 ```
 
diff --git a/src/trees/underlying-trees-elements-coalgebras-polynomial-endofunctors.lagda.md b/src/trees/underlying-trees-elements-coalgebras-polynomial-endofunctors.lagda.md
index fbb4544f83..1de2c5aa49 100644
--- a/src/trees/underlying-trees-elements-coalgebras-polynomial-endofunctors.lagda.md
+++ b/src/trees/underlying-trees-elements-coalgebras-polynomial-endofunctors.lagda.md
@@ -287,7 +287,7 @@ embedding. The total space `Σ (y : B x), node-element-coalgebra' (α y)` embeds
 into `node-element-coalgebra' (tree-coalgebra x α)`, and this implies that the
 node inclusion has the same truncation level as the fiber inclusions
 
-```md
+```text
   node-element-coalgebra' (α b) → Σ (y : B x), node-element-coalgebra' (α y)
 ```
 
diff --git a/src/trees/w-type-of-natural-numbers.lagda.md b/src/trees/w-type-of-natural-numbers.lagda.md
index 656546a393..7bc2981e8f 100644
--- a/src/trees/w-type-of-natural-numbers.lagda.md
+++ b/src/trees/w-type-of-natural-numbers.lagda.md
@@ -31,7 +31,7 @@ open import trees.w-types
 Since the type of natural numbers is an initial algebra for the polynomial
 endofunctor
 
-```md
+```text
   X ↦ X + 𝟙,
 ```
 
diff --git a/src/type-theories/dependent-type-theories.lagda.md b/src/type-theories/dependent-type-theories.lagda.md
index 167d0a9d50..eab2f62584 100644
--- a/src/type-theories/dependent-type-theories.lagda.md
+++ b/src/type-theories/dependent-type-theories.lagda.md
@@ -31,7 +31,7 @@ algebraic theories.
 (Dependency) systems are the structure around which a dependent type theory is
 built.
 
-```md
+```text
     Ã₀       Ã₁       Ã₂
     |        |        |
     |        |        |
@@ -582,7 +582,7 @@ preserve generic elements.
 For example, the rule that states that weakening preserves weakening (on types)
 can be displayed as follows:
 
-```md
+```text
         Γ ⊢ A type          Γ,Δ ⊢ B type          Γ,Δ,Ε ⊢ C type
   ------------------------------------------------------------------------
   Γ,A,W(A,Δ),W(A,B),W(W(A,B),W(A,E)) ⊢ W(W(A,B),W(A,C))=W(A,W(B,C)) type
diff --git a/src/univalent-combinatorics/counting-dependent-pair-types.lagda.md b/src/univalent-combinatorics/counting-dependent-pair-types.lagda.md
index 7a84bd5ad1..02a84f045b 100644
--- a/src/univalent-combinatorics/counting-dependent-pair-types.lagda.md
+++ b/src/univalent-combinatorics/counting-dependent-pair-types.lagda.md
@@ -169,7 +169,7 @@ counted if and only if the type `Σ A (¬ ∘ B)` can be counted. However, to av
 having to invoke function extensionality, we show that if `Σ A B` and each `B x`
 can be counted, then `A` can be counted if and only if
 
-```md
+```text
    count (Σ A (λ x → is-zero-ℕ (number-of-elements-count (f x)))),
 ```
 
diff --git a/src/univalent-combinatorics/finite-presentations.lagda.md b/src/univalent-combinatorics/finite-presentations.lagda.md
index 94f2f33ec7..a072941ed2 100644
--- a/src/univalent-combinatorics/finite-presentations.lagda.md
+++ b/src/univalent-combinatorics/finite-presentations.lagda.md
@@ -17,7 +17,7 @@ module univalent-combinatorics.finite-presentations where
 Finitely presented types are types A equipped with a map f : Fin k → A such that
 the composite
 
-```md
+```text
   Fin k → A → type-trunc-Set A
 ```