Swap from md to text code blocks (#622)

- Fix diagrams in `pullback-hom`
- Swap from `md` to `text` code blocks
- Register Collatz' bijection in the OEIS file

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₁
             |                        |

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

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

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
 ```
 

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
 ```
 

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
 ```
 

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ⁿ⁻ⁱ.
 ```
 

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ⁿ⁻ⁱ.
 ```
 

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).
 ```
 

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.
 ```
 

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.
 ```
 

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

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
 ```
 

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)
 ```
 

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 ∥.
 ```
 

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
   |           |

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
   |  \       ^  |
   |    \   /    |

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
   |  \       ^  |
   |    \   /    |

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
             *
           / | \
          /  |  \

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
   |         |
   |         |

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
   \     /
    \   /

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
   \     /
    \   /

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
   |        |

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)))
 ```
 

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

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

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

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

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
   |        |        |
   |        |        |

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
 ```

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)

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'
 ```
 

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
       |         |

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
   \     /
    \   /

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
  |        |        |

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)
 ```
 

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)
 ```
 

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))
 ```
 

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
   |          |

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
   |          |

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