diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml
index 7df9e33a14..6934ffd1cd 100644
--- a/.github/workflows/ci.yaml
+++ b/.github/workflows/ci.yaml
@@ -34,7 +34,7 @@ jobs:
         agda: ['2.7.0']
     steps:
       - name: Checkout our repository
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           path: master
       - name: Setup Agda
@@ -42,7 +42,7 @@ jobs:
         with:
           agda-version: ${{ matrix.agda }}
 
-      - uses: actions/cache/restore@v3
+      - uses: actions/cache/restore@v4
         id: cache-agda-formalization
         name: Restore Agda formalization cache
         with:
@@ -61,13 +61,13 @@ jobs:
           make check
 
       - name: Save Agda build cache
-        uses: actions/cache/save@v3
+        uses: actions/cache/save@v4
         with:
           path: master/_build
           key: '${{ steps.cache-agda-formalization.outputs.cache-primary-key }}'
 
       # Install Python and friends for website generation only where needed
-      - uses: actions/setup-python@v4
+      - uses: actions/setup-python@v5
         if: ${{ matrix.os == 'ubuntu-latest' }}
         with:
           python-version: '3.8'
@@ -92,7 +92,7 @@ jobs:
       # keep the same key for a branch and update it on pushes.
       - name: Save pre-website cache
         if: ${{ matrix.os == 'ubuntu-latest' }}
-        uses: actions/cache/save@v3
+        uses: actions/cache/save@v4
         with:
           key: pre-website-${{ github.run_id }}
           path: master/docs
@@ -106,21 +106,21 @@ jobs:
       actions: write
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
         with:
           path: master
 
-      - uses: peaceiris/actions-mdbook@v1
+      - uses: peaceiris/actions-mdbook@v2
         with:
           mdbook-version: '0.4.34'
 
-      - uses: baptiste0928/cargo-install@v2
+      - uses: baptiste0928/cargo-install@v3
         with:
           crate: mdbook-linkcheck
           version: '0.7.7'
 
       # Install Python and friends for website generation only where needed
-      - uses: actions/setup-python@v4
+      - uses: actions/setup-python@v5
         with:
           python-version: '3.8'
           check-latest: true
@@ -128,7 +128,7 @@ jobs:
 
       - run: python3 -m pip install -r master/scripts/requirements.txt
 
-      - uses: actions/cache/restore@v3
+      - uses: actions/cache/restore@v4
         with:
           key: pre-website-${{ github.run_id }}
           path: master/docs
@@ -162,9 +162,9 @@ jobs:
   pre-commit:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
 
-      - uses: actions/setup-python@v4
+      - uses: actions/setup-python@v5
         with:
           python-version: '3.8'
           check-latest: true
@@ -172,4 +172,4 @@ jobs:
 
       - run: python3 -m pip install -r scripts/requirements.txt
 
-      - uses: pre-commit/action@v3.0.0
+      - uses: pre-commit/action@v3.0.1
diff --git a/.github/workflows/clean-up.yaml b/.github/workflows/clean-up.yaml
index 6ed7f6058c..4ffe5905ca 100644
--- a/.github/workflows/clean-up.yaml
+++ b/.github/workflows/clean-up.yaml
@@ -9,7 +9,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Check out code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Cleanup
         run: |
diff --git a/.github/workflows/pages.yaml b/.github/workflows/pages.yaml
index 0c238de0e1..0ab93274bc 100644
--- a/.github/workflows/pages.yaml
+++ b/.github/workflows/pages.yaml
@@ -32,7 +32,7 @@ jobs:
       id-token: write # to verify the deployment originates from an appropriate source
     steps:
       - name: Checkout our repository
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           path: master
           # We need the entire history for contributor information
@@ -43,7 +43,7 @@ jobs:
         with:
           agda-version: ${{ matrix.agda }}
 
-      - uses: actions/cache/restore@v3
+      - uses: actions/cache/restore@v4
         id: cache-agda-formalization
         name: Restore Agda formalization cache
         with:
@@ -56,35 +56,35 @@ jobs:
 
       # Keep versions in sync with the Makefile
       - name: MDBook setup
-        uses: peaceiris/actions-mdbook@v1
+        uses: peaceiris/actions-mdbook@v2
         with:
           mdbook-version: '0.4.34'
 
       - name: Install mdbook-pagetoc
-        uses: baptiste0928/cargo-install@v2
+        uses: baptiste0928/cargo-install@v3
         with:
           crate: mdbook-pagetoc
           version: '0.1.7'
 
       - name: Install mdbook-katex
-        uses: baptiste0928/cargo-install@v2
+        uses: baptiste0928/cargo-install@v3
         with:
           crate: mdbook-katex
           version: '0.5.7'
 
       - name: Install mdbook-linkcheck
-        uses: baptiste0928/cargo-install@v2
+        uses: baptiste0928/cargo-install@v3
         with:
           crate: mdbook-linkcheck
           version: '0.7.7'
 
       - name: Install mdbook-catppuccin
-        uses: baptiste0928/cargo-install@v2
+        uses: baptiste0928/cargo-install@v3
         with:
           crate: mdbook-catppuccin
           version: '1.2.0'
 
-      - uses: actions/setup-python@v4
+      - uses: actions/setup-python@v5
         with:
           python-version: '3.8'
           check-latest: true
@@ -100,13 +100,13 @@ jobs:
           make website
 
       - name: Setup Pages
-        uses: actions/configure-pages@v3
+        uses: actions/configure-pages@v5
         if: >-
           github.ref == 'refs/heads/master' || github.event_name ==
           'workflow_dispatch'
 
       - name: Upload artifact
-        uses: actions/upload-pages-artifact@v1
+        uses: actions/upload-pages-artifact@v3
         if: >-
           github.ref == 'refs/heads/master' || github.event_name ==
           'workflow_dispatch'
@@ -114,7 +114,7 @@ jobs:
           path: master/book/html
 
       - name: Deploy to GitHub Pages
-        uses: actions/deploy-pages@v1
+        uses: actions/deploy-pages@v4
         id: deployment
         if: >-
           github.ref == 'refs/heads/master' || github.event_name ==
diff --git a/.github/workflows/profiling.yaml b/.github/workflows/profiling.yaml
index 2b12997f87..95db9d7d2d 100644
--- a/.github/workflows/profiling.yaml
+++ b/.github/workflows/profiling.yaml
@@ -19,7 +19,7 @@ jobs:
 
     steps:
       - name: Checkout our repository
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           path: repo
 
diff --git a/agda-unimath.agda-lib b/agda-unimath.agda-lib
index 2de2f04aa9..4404561421 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
+flags: --without-K --exact-split --no-import-sorts --auto-inline --no-require-unique-meta-solutions -WnoWithoutKFlagPrimEraseEquality --no-postfix-projections
diff --git a/src/category-theory/conservative-functors-precategories.lagda.md b/src/category-theory/conservative-functors-precategories.lagda.md
index 0116f42e94..bdbd787dcb 100644
--- a/src/category-theory/conservative-functors-precategories.lagda.md
+++ b/src/category-theory/conservative-functors-precategories.lagda.md
@@ -22,8 +22,9 @@ open import foundation.universe-levels
 ## Idea
 
 A [functor](category-theory.functors-precategories.md) `F : C → D` between
-[precategories](category-theory.precategories.md) is **conservative** if every
-morphism that is mapped to an
+[precategories](category-theory.precategories.md) is
+{{#concept "conservative" Disambiguation="functor of set-level precategories" WDID=Q23808682 WD="conservative functor" Agda=is-conservative-functor-Precategory Agda=conservative-functor-Precategory}}
+if every morphism that is mapped to an
 [isomorphism](category-theory.isomorphisms-in-precategories.md) in `D` is an
 isomorphism in `C`.
 
diff --git a/src/category-theory/essentially-surjective-functors-precategories.lagda.md b/src/category-theory/essentially-surjective-functors-precategories.lagda.md
index b33efd03a0..da79c73d46 100644
--- a/src/category-theory/essentially-surjective-functors-precategories.lagda.md
+++ b/src/category-theory/essentially-surjective-functors-precategories.lagda.md
@@ -22,7 +22,8 @@ open import foundation.universe-levels
 ## Idea
 
 A [functor](category-theory.functors-precategories.md) `F : C → D` between
-[precategories](category-theory.precategories.md) is **essentially surjective**
+[precategories](category-theory.precategories.md) is
+{{#concept "essentially surjective" Disambiguation="functor between set-level precategories" WDID=Q140283 WD="essentially surjective functor" Agda=is-essentially-surjective-functor-Precategory Agda=essentially-surjective-functor-Precategory}}
 if there for every object `y : D`
 [merely exists](foundation.existential-quantification.md) an object `x : C` such
 that `F x ≅ y`.
diff --git a/src/category-theory/pseudomonic-functors-precategories.lagda.md b/src/category-theory/pseudomonic-functors-precategories.lagda.md
index 8dacf40fbd..12821ec3b4 100644
--- a/src/category-theory/pseudomonic-functors-precategories.lagda.md
+++ b/src/category-theory/pseudomonic-functors-precategories.lagda.md
@@ -43,7 +43,7 @@ Pseudomonic functors present
 is the "right notion" of subcategory with respect to the _principle of
 invariance under equivalences_.
 
-## Definition
+## Definitions
 
 ### The predicate on isomorphisms of being full
 
diff --git a/src/category-theory/split-essentially-surjective-functors-precategories.lagda.md b/src/category-theory/split-essentially-surjective-functors-precategories.lagda.md
index 2c369636ce..d62ed8e8fe 100644
--- a/src/category-theory/split-essentially-surjective-functors-precategories.lagda.md
+++ b/src/category-theory/split-essentially-surjective-functors-precategories.lagda.md
@@ -7,16 +7,26 @@ module category-theory.split-essentially-surjective-functors-precategories where
 <details><summary>Imports</summary>
 
 ```agda
+open import category-theory.categories
+open import category-theory.cores-precategories
 open import category-theory.essential-fibers-of-functors-precategories
 open import category-theory.essentially-surjective-functors-precategories
+open import category-theory.fully-faithful-functors-precategories
 open import category-theory.functors-precategories
+open import category-theory.isomorphisms-in-categories
 open import category-theory.isomorphisms-in-precategories
 open import category-theory.precategories
+open import category-theory.pseudomonic-functors-precategories
 
+open import foundation.contractible-types
 open import foundation.dependent-pair-types
+open import foundation.equivalences
 open import foundation.function-types
 open import foundation.functoriality-dependent-pair-types
 open import foundation.propositional-truncations
+open import foundation.propositions
+open import foundation.retracts-of-types
+open import foundation.sections
 open import foundation.universe-levels
 ```
 
@@ -25,8 +35,9 @@ open import foundation.universe-levels
 ## Idea
 
 A [functor](category-theory.functors-precategories.md) `F : C → D` between
-[precategories](category-theory.precategories.md) is **split essentially
-surjective** if there is a section of the
+[precategories](category-theory.precategories.md) is
+{{#concept "split essentially surjective" Disambiguation="functor between set-level precategories" Agda=is-split-essentially-surjective-functor-Precategory  Agda=split-essentially-surjective-functor-Precategory}}
+if there is a section of the
 [essential fiber](category-theory.essential-fibers-of-functors-precategories.md)
 over every object of `D`.
 
@@ -166,14 +177,110 @@ module _
       ( is-essentially-surjective-is-split-essentially-surjective-functor-Precategory)
 ```
 
-### Being split essentially surjective is a property of fully faithful functors when the codomain is a category
+### Being split essentially surjective is a property of fully faithful functors when the domain is a category
 
-This remains to be shown. This is Lemma 6.8 of _Univalent Categories and the
-Rezk completion_.
+This is Lemma 6.8 of {{#cite AKS15}}, although we give a different proof.
+
+**Proof.** Let `F : 𝒞 → 𝒟` be a functor of precategories, where `𝒞` is
+univalent. It suffices to assume `F` is fully faithful on the
+[core](category-theory.cores-categories.md) of `𝒞`. Then, to show that
+`is-split-essentially-surjective` is a proposition, i.e., that
+
+```text
+  (d : 𝒟₀) → Σ (x : 𝒞₀), (Fx ≅ d)
+```
+
+is a proposition it is equivalent to show that if it has an element it is
+contractible, so assume `F` is split essentially surjective. Then, it suffices
+to show that for every `d : 𝒟₀`, the type `Σ (x : 𝒞₀), (Fx ≅ d)` is
+contractible. By split essential surjectivity there is an element `y : 𝒞₀` such
+that `Fy ≅ d` and since postcomposing by an isomorphism is an equivalence of
+isomorphism-sets, we have
+
+```text
+  (Fx ≅ d) ≃ (Fx ≅ Fy) ≃ (x ≅ y)
+```
+
+so `(Σ (x : 𝒞₀), (Fx ≅ d)) ≃ (Σ (x : 𝒞₀), (x ≅ y))`, and the latter is
+contractible by univalence.
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (C : Precategory l1 l2) (D : Precategory l3 l4)
+  (F : functor-Precategory C D)
+  (c : is-category-Precategory C)
+  where
+
+  is-proof-irrelevant-is-split-essentially-surjective-has-section-on-isos-functor-is-category-domain-Precategory :
+    ( (x y : obj-Precategory C) →
+      section (preserves-iso-functor-Precategory C D F {x} {y})) →
+    is-proof-irrelevant
+      ( is-split-essentially-surjective-functor-Precategory C D F)
+  is-proof-irrelevant-is-split-essentially-surjective-has-section-on-isos-functor-is-category-domain-Precategory
+    H s =
+    is-contr-Π
+      ( λ d →
+        is-contr-retract-of
+          ( Σ (obj-Category (C , c)) (iso-Category (C , c) (pr1 (s d))))
+          ( retract-tot
+            ( λ x →
+              comp-retract
+                ( retract-section
+                  ( preserves-iso-functor-Precategory C D F)
+                  ( H (pr1 (s d)) x))
+                ( retract-equiv
+                  ( equiv-inv-iso-Precategory D ∘e
+                    equiv-postcomp-hom-iso-Precategory
+                      ( core-precategory-Precategory D)
+                      ( map-equiv
+                        ( compute-iso-core-Precategory D)
+                        ( inv-iso-Precategory D (pr2 (s d))))
+                      ( obj-functor-Precategory C D F x)))))
+          ( is-torsorial-iso-Category (C , c) (pr1 (s d))))
+
+  is-prop-is-split-essentially-surjective-has-section-on-isos-functor-is-category-domain-Precategory :
+    ( (x y : obj-Precategory C) →
+      section (preserves-iso-functor-Precategory C D F {x} {y})) →
+    is-prop
+      ( is-split-essentially-surjective-functor-Precategory C D F)
+  is-prop-is-split-essentially-surjective-has-section-on-isos-functor-is-category-domain-Precategory
+    =
+    is-prop-is-proof-irrelevant ∘
+    is-proof-irrelevant-is-split-essentially-surjective-has-section-on-isos-functor-is-category-domain-Precategory
+
+  is-prop-is-split-essentially-surjective-is-fully-faithful-on-isos-functor-is-category-domain-Precategory :
+    ( (x y : obj-Precategory C) →
+      is-equiv (preserves-iso-functor-Precategory C D F {x} {y})) →
+    is-prop (is-split-essentially-surjective-functor-Precategory C D F)
+  is-prop-is-split-essentially-surjective-is-fully-faithful-on-isos-functor-is-category-domain-Precategory
+    H =
+    is-prop-is-split-essentially-surjective-has-section-on-isos-functor-is-category-domain-Precategory
+      ( λ x y → section-is-equiv (H x y))
+
+  is-prop-is-split-essentially-surjective-is-pseudomonic-functor-is-category-domain-Precategory :
+    is-pseudomonic-functor-Precategory C D F →
+    is-prop (is-split-essentially-surjective-functor-Precategory C D F)
+  is-prop-is-split-essentially-surjective-is-pseudomonic-functor-is-category-domain-Precategory
+    H =
+    is-prop-is-split-essentially-surjective-is-fully-faithful-on-isos-functor-is-category-domain-Precategory
+      ( λ x y →
+        is-equiv-preserves-iso-is-pseudomonic-functor-Precategory C D F H
+          { x}
+          { y})
+
+  is-prop-is-split-essentially-surjective-is-fully-faithful-functor-is-category-domain-Precategory :
+    is-fully-faithful-functor-Precategory C D F →
+    is-prop (is-split-essentially-surjective-functor-Precategory C D F)
+  is-prop-is-split-essentially-surjective-is-fully-faithful-functor-is-category-domain-Precategory
+    H =
+    is-prop-is-split-essentially-surjective-is-pseudomonic-functor-is-category-domain-Precategory
+      ( is-pseudomonic-is-fully-faithful-functor-Precategory C D F H)
+```
 
 ## References
 
-{{#bibliography}} {{#reference AKS15}}
+{{#bibliography}}
 
 ## External links
 
diff --git a/src/foundation-core/retracts-of-types.lagda.md b/src/foundation-core/retracts-of-types.lagda.md
index 41e3177933..43c71c5134 100644
--- a/src/foundation-core/retracts-of-types.lagda.md
+++ b/src/foundation-core/retracts-of-types.lagda.md
@@ -84,6 +84,11 @@ module _
   section-retract : section map-retraction-retract
   pr1 section-retract = inclusion-retract
   pr2 section-retract = is-retraction-map-retraction-retract
+
+retract-section :
+  {l1 l2 : Level} {A : UU l1} {B : UU l2}
+  (f : A → B) → section f → B retract-of A
+retract-section f s = (pr1 s , f , pr2 s)
 ```
 
 ### The type of retracts of a type
diff --git a/src/foundation/commuting-cubes-of-maps.lagda.md b/src/foundation/commuting-cubes-of-maps.lagda.md
index 9135953cfe..0309bafe4b 100644
--- a/src/foundation/commuting-cubes-of-maps.lagda.md
+++ b/src/foundation/commuting-cubes-of-maps.lagda.md
@@ -9,6 +9,7 @@ module foundation.commuting-cubes-of-maps where
 ```agda
 open import foundation.action-on-identifications-functions
 open import foundation.commuting-hexagons-of-identifications
+open import foundation.commuting-squares-of-homotopies
 open import foundation.commuting-squares-of-maps
 open import foundation.cones-over-cospan-diagrams
 open import foundation.dependent-pair-types
@@ -16,6 +17,7 @@ open import foundation.function-extensionality
 open import foundation.homotopies
 open import foundation.universe-levels
 open import foundation.whiskering-homotopies-composition
+open import foundation.whiskering-homotopies-concatenation
 
 open import foundation-core.function-types
 open import foundation-core.identity-types
@@ -51,7 +53,7 @@ of maps has a top face, a back-left face, a back-right face, a front-left face,
 a front-right face, and a bottom face, all of which are homotopies. An element
 of type `coherence-cube-maps` is a homotopy filling the cube.
 
-## Definition
+## Definitions
 
 ```agda
 module _
@@ -317,6 +319,113 @@ expect to be able to construct a coherence
       ( inv-htpy back-left)
 ```
 
+### Vertical pasting of commuting cubes
+
+```agda
+module _
+  {l1 l2 l3 l4 l1' l2' l3' l4' l1'' l2'' l3'' l4'' : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
+  (f : A → B) (g : A → C) (h : B → D) (k : C → D)
+  {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
+  (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
+  {A'' : UU l1''} {B'' : UU l2''} {C'' : UU l3''} {D'' : UU l4''}
+  (f'' : A'' → B'') (g'' : A'' → C'') (h'' : B'' → D'') (k'' : C'' → D'')
+  (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
+  (hA' : A'' → A') (hB' : B'' → B') (hC' : C'' → C') (hD' : D'' → D')
+  (mid : (h' ∘ f') ~ (k' ∘ g'))
+  (bottom-back-left : (f ∘ hA) ~ (hB ∘ f'))
+  (bottom-back-right : (g ∘ hA) ~ (hC ∘ g'))
+  (bottom-front-left : (h ∘ hB) ~ (hD ∘ h'))
+  (bottom-front-right : (k ∘ hC) ~ (hD ∘ k'))
+  (bottom : (h ∘ f) ~ (k ∘ g))
+  (top : (h'' ∘ f'') ~ (k'' ∘ g''))
+  (top-back-left : (f' ∘ hA') ~ (hB' ∘ f''))
+  (top-back-right : (g' ∘ hA') ~ (hC' ∘ g''))
+  (top-front-left : (h' ∘ hB') ~ (hD' ∘ h''))
+  (top-front-right : (k' ∘ hC') ~ (hD' ∘ k''))
+  where
+
+  pasting-vertical-coherence-cube-maps :
+    coherence-cube-maps f g h k f' g' h' k' hA hB hC hD
+      ( mid)
+      ( bottom-back-left)
+      ( bottom-back-right)
+      ( bottom-front-left)
+      ( bottom-front-right)
+      ( bottom) →
+    coherence-cube-maps f' g' h' k' f'' g'' h'' k'' hA' hB' hC' hD'
+      ( top)
+      ( top-back-left)
+      ( top-back-right)
+      ( top-front-left)
+      ( top-front-right)
+      ( mid) →
+    coherence-cube-maps f g h k f'' g'' h'' k''
+      ( hA ∘ hA') (hB ∘ hB') (hC ∘ hC') (hD ∘ hD')
+      ( top)
+      ( pasting-vertical-coherence-square-maps f'' hA' hB' f' hA hB f
+        ( top-back-left) (bottom-back-left))
+      ( pasting-vertical-coherence-square-maps g'' hA' hC' g' hA hC g
+        ( top-back-right) (bottom-back-right))
+      ( pasting-vertical-coherence-square-maps h'' hB' hD' h' hB hD h
+        ( top-front-left) (bottom-front-left))
+      ( pasting-vertical-coherence-square-maps k'' hC' hD' k' hC hD k
+        ( top-front-right) (bottom-front-right))
+      ( bottom)
+  pasting-vertical-coherence-cube-maps α β =
+    ( right-whisker-concat-htpy
+      ( commutative-pasting-vertical-pasting-horizontal-coherence-square-maps
+        f'' h'' hA' hB' hD' f' h' hA hB hD f h
+        top-back-left top-front-left bottom-back-left bottom-front-left)
+      ( (hD ∘ hD') ·l top)) ∙h
+    ( left-whisker-concat-coherence-square-homotopies
+      ( bottom-left-rect ·r hA')
+      ( hD ·l (mid ·r hA'))
+      ( hD ·l top-left-rect)
+      ( hD ·l top-right-rect)
+      ( (hD ∘ hD') ·l top)
+      ( ( left-whisker-concat-htpy
+          ( hD ·l top-left-rect)
+          ( inv-preserves-comp-left-whisker-comp hD hD' top)) ∙h
+        ( map-coherence-square-homotopies hD
+          ( mid ·r hA') (top-left-rect) (top-right-rect) (hD' ·l top)
+          ( β)))) ∙h
+    ( right-whisker-concat-htpy
+      ( α ·r hA')
+      ( hD ·l top-right-rect)) ∙h
+    ( assoc-htpy
+      ( bottom ·r (hA ∘ hA'))
+      ( bottom-right-rect ·r hA')
+      ( hD ·l top-right-rect)) ∙h
+    ( left-whisker-concat-htpy
+      ( bottom ·r (hA ∘ hA'))
+      ( inv-htpy
+        ( commutative-pasting-vertical-pasting-horizontal-coherence-square-maps
+          g'' k'' hA' hC' hD' g' k' hA hC hD g k
+          top-back-right top-front-right bottom-back-right bottom-front-right)))
+    where
+      bottom-left-rect : h ∘ f ∘ hA ~ hD ∘ h' ∘ f'
+      bottom-left-rect =
+        pasting-horizontal-coherence-square-maps f' h' hA hB hD f h
+          bottom-back-left bottom-front-left
+      bottom-right-rect : k ∘ g ∘ hA ~ hD ∘ k' ∘ g'
+      bottom-right-rect =
+        pasting-horizontal-coherence-square-maps g' k' hA hC hD g k
+          bottom-back-right bottom-front-right
+      top-left-rect : h' ∘ f' ∘ hA' ~ hD' ∘ h'' ∘ f''
+      top-left-rect =
+        pasting-horizontal-coherence-square-maps f'' h'' hA' hB' hD' f' h'
+          top-back-left top-front-left
+      top-right-rect : k' ∘ g' ∘ hA' ~ hD' ∘ k'' ∘ g''
+      top-right-rect =
+        pasting-horizontal-coherence-square-maps g'' k'' hA' hC' hD' g' k'
+          top-back-right top-front-right
+      back-left-rect : f ∘ hA ∘ hA' ~ hB ∘ hB' ∘ f''
+      back-left-rect =
+        pasting-vertical-coherence-square-maps f'' hA' hB' f' hA hB f
+          top-back-left bottom-back-left
+```
+
 ### Any coherence of commuting cubes induces a coherence of parallel cones
 
 ```agda
diff --git a/src/order-theory.lagda.md b/src/order-theory.lagda.md
index 508171dcb4..a5f5985c0f 100644
--- a/src/order-theory.lagda.md
+++ b/src/order-theory.lagda.md
@@ -120,11 +120,11 @@ open import order-theory.top-elements-posets public
 open import order-theory.top-elements-preorders public
 open import order-theory.total-orders public
 open import order-theory.total-preorders public
+open import order-theory.transitive-well-founded-relations public
 open import order-theory.upper-bounds-chains-posets public
 open import order-theory.upper-bounds-large-posets public
 open import order-theory.upper-bounds-posets public
 open import order-theory.upper-sets-large-posets public
-open import order-theory.well-founded-orders public
 open import order-theory.well-founded-relations public
 open import order-theory.zorns-lemma public
 ```
diff --git a/src/order-theory/accessible-elements-relations.lagda.md b/src/order-theory/accessible-elements-relations.lagda.md
index 122fbfe205..a6b6863dca 100644
--- a/src/order-theory/accessible-elements-relations.lagda.md
+++ b/src/order-theory/accessible-elements-relations.lagda.md
@@ -22,10 +22,11 @@ open import foundation-core.propositions
 ## Idea
 
 Given a type `X` with a [binary relation](foundation.binary-relations.md)
-`_<_ : X → X → Type` we say that `x : X` is **accessible** if `y` is accessible
-for all `y < x`. Note that the predicate of being an accessible element is a
-recursive condition. The accessibility predicate is therefore implemented as an
-inductive type with one constructor:
+`_<_ : X → X → Type` we say that `x : X` is
+{{#concept "accessible" Disambiguation="element with respect to a binary relation" Agda=is-accessible-element-Relation}}
+if, recursively, `y` is accessible for all `y < x`. Since the accessibility
+predicate is defined recursively, it is implemented as an inductive type with
+one constructor:
 
 ```text
   access : ((y : X) → y < x → is-accessible y) → is-accessible x
@@ -37,7 +38,7 @@ inductive type with one constructor:
 
 ```agda
 module _
-  {l1 l2} {X : UU l1} (_<_ : Relation l2 X)
+  {l1 l2 : Level} {X : UU l1} (_<_ : Relation l2 X)
   where
 
   data is-accessible-element-Relation (x : X) : UU (l1 ⊔ l2)
@@ -70,8 +71,7 @@ module _
   is-accessible-element-is-related-to-accessible-element-Relation :
     {x : X} → is-accessible-element-Relation _<_ x →
     {y : X} → y < x → is-accessible-element-Relation _<_ y
-  is-accessible-element-is-related-to-accessible-element-Relation (access f) =
-    f
+  is-accessible-element-is-related-to-accessible-element-Relation (access f) = f
 ```
 
 ### An induction principle for accessible elements
@@ -112,7 +112,9 @@ are equal. Therefore it follows that `f ＝ f'`, and we conclude that
 `access f ＝ access f'`.
 
 ```agda
-module _ {l1 l2} {X : UU l1} (_<_ : Relation l2 X) where
+module _
+  {l1 l2 : Level} {X : UU l1} (_<_ : Relation l2 X)
+  where
 
   all-elements-equal-is-accessible-element-Relation :
     (x : X) → all-elements-equal (is-accessible-element-Relation _<_ x)
diff --git a/src/order-theory/incidence-algebras.lagda.md b/src/order-theory/incidence-algebras.lagda.md
index 3ce4a89e69..f96b061659 100644
--- 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
 
diff --git a/src/order-theory/ordinals.lagda.md b/src/order-theory/ordinals.lagda.md
index 06b3979006..7dc9994603 100644
--- a/src/order-theory/ordinals.lagda.md
+++ b/src/order-theory/ordinals.lagda.md
@@ -10,9 +10,15 @@ module order-theory.ordinals where
 open import foundation.binary-relations
 open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.logical-equivalences
+open import foundation.propositions
+open import foundation.sets
 open import foundation.universe-levels
 
-open import order-theory.well-founded-orders
+open import order-theory.posets
+open import order-theory.preorders
+open import order-theory.transitive-well-founded-relations
 open import order-theory.well-founded-relations
 ```
 
@@ -20,18 +26,33 @@ open import order-theory.well-founded-relations
 
 ## Idea
 
-An ordinal is a propositional relation that is
+An
+{{#concept "ordinal" WDID=Q191780 WD="ordinal number" Agda=is-ordinal Agda=Ordinal}}
+is a type `X` [equipped](foundation.structure.md) with a
+[propositional](foundation-core.propositions.md)
+[relation](foundation.binary-relations.md) `_<_` that is
 
-- Transitive: `R x y` and `R y z` imply `R x y`.
-- Extensional: `R x y` and `R y x` imply `x ＝ y`.
-- Well-founded: a structure on which it is well-defined to do induction.
+- **Well-founded:** a structure on which it is well-defined to do induction.
+- **Transitive:** if `x < y` and `y < z` then `x < z`.
+- **Extensional:** `x ＝ y` precisely if they are greater than the same
+  elements.
 
 In other words, it is a
-[well-founded order](order-theory.well-founded-orders.md) that is `Prop`-valued
-and antisymmetric.
+[transitive well-founded relation](order-theory.transitive-well-founded-relations.md)
+that is `Prop`-valued and extensional.
 
 ## Definitions
 
+### The extensionality principle of ordinals
+
+```agda
+extensionality-principle-Ordinal :
+  {l1 l2 : Level} {X : UU l1} → Relation-Prop l2 X → UU (l1 ⊔ l2)
+extensionality-principle-Ordinal {X = X} R =
+  (x y : X) →
+  ((u : X) → type-Relation-Prop R u x ↔ type-Relation-Prop R u y) → x ＝ y
+```
+
 ### The predicate of being an ordinal
 
 ```agda
@@ -41,61 +62,113 @@ module _
 
   is-ordinal : UU (l1 ⊔ l2)
   is-ordinal =
-    is-well-founded-order-Relation (type-Relation-Prop R) ×
-    is-antisymmetric (type-Relation-Prop R)
+    ( is-transitive-well-founded-relation-Relation (type-Relation-Prop R)) ×
+    ( extensionality-principle-Ordinal R)
 ```
 
-### Ordinals
+### The type of ordinals
 
 ```agda
-Ordinal : {l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2)
-Ordinal l2 X = Σ (Relation-Prop l2 X) is-ordinal
+Ordinal : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+Ordinal l1 l2 = Σ (UU l1) (λ X → Σ (Relation-Prop l2 X) is-ordinal)
 
 module _
-  {l1 l2 : Level} {X : UU l1} (S : Ordinal l2 X)
+  {l1 l2 : Level} (O : Ordinal l1 l2)
   where
 
-  lt-prop-Ordinal : Relation-Prop l2 X
-  lt-prop-Ordinal = pr1 S
-
-  lt-Ordinal : Relation l2 X
-  lt-Ordinal = type-Relation-Prop lt-prop-Ordinal
-
-  is-ordinal-Ordinal :
-    is-ordinal lt-prop-Ordinal
-  is-ordinal-Ordinal = pr2 S
-
-  is-well-founded-order-Ordinal :
-    is-well-founded-order-Relation lt-Ordinal
-  is-well-founded-order-Ordinal = pr1 is-ordinal-Ordinal
-
-  is-antisymmetric-Ordinal :
-    is-antisymmetric lt-Ordinal
-  is-antisymmetric-Ordinal = pr2 is-ordinal-Ordinal
-
-  is-transitive-Ordinal : is-transitive lt-Ordinal
-  is-transitive-Ordinal =
-    pr1 is-well-founded-order-Ordinal
-
-  is-well-founded-relation-Ordinal :
-    is-well-founded-Relation lt-Ordinal
-  is-well-founded-relation-Ordinal =
-    pr2 is-well-founded-order-Ordinal
-
-  well-founded-relation-Ordinal : Well-Founded-Relation l2 X
-  pr1 well-founded-relation-Ordinal =
-    lt-Ordinal
-  pr2 well-founded-relation-Ordinal =
-    is-well-founded-relation-Ordinal
-
-  is-asymmetric-Ordinal :
-    is-asymmetric lt-Ordinal
-  is-asymmetric-Ordinal =
-    is-asymmetric-Well-Founded-Relation well-founded-relation-Ordinal
-
-  is-irreflexive-Ordinal :
-    is-irreflexive lt-Ordinal
-  is-irreflexive-Ordinal =
-    is-irreflexive-Well-Founded-Relation
-      ( well-founded-relation-Ordinal)
+  type-Ordinal : UU l1
+  type-Ordinal = pr1 O
+
+  le-prop-Ordinal : Relation-Prop l2 type-Ordinal
+  le-prop-Ordinal = pr1 (pr2 O)
+
+  le-Ordinal : Relation l2 type-Ordinal
+  le-Ordinal = type-Relation-Prop le-prop-Ordinal
+
+  is-ordinal-Ordinal : is-ordinal le-prop-Ordinal
+  is-ordinal-Ordinal = pr2 (pr2 O)
+
+  is-transitive-well-founded-relation-le-Ordinal :
+    is-transitive-well-founded-relation-Relation le-Ordinal
+  is-transitive-well-founded-relation-le-Ordinal = pr1 is-ordinal-Ordinal
+
+  transitive-well-founded-relation-Ordinal :
+    Transitive-Well-Founded-Relation l2 type-Ordinal
+  transitive-well-founded-relation-Ordinal =
+    ( le-Ordinal , is-transitive-well-founded-relation-le-Ordinal)
+
+  is-extensional-Ordinal : extensionality-principle-Ordinal le-prop-Ordinal
+  is-extensional-Ordinal = pr2 is-ordinal-Ordinal
+
+  is-transitive-le-Ordinal : is-transitive le-Ordinal
+  is-transitive-le-Ordinal =
+    is-transitive-le-Transitive-Well-Founded-Relation
+      transitive-well-founded-relation-Ordinal
+
+  is-well-founded-relation-le-Ordinal : is-well-founded-Relation le-Ordinal
+  is-well-founded-relation-le-Ordinal =
+    is-well-founded-relation-le-Transitive-Well-Founded-Relation
+      transitive-well-founded-relation-Ordinal
+
+  well-founded-relation-Ordinal : Well-Founded-Relation l2 type-Ordinal
+  well-founded-relation-Ordinal =
+    well-founded-relation-Transitive-Well-Founded-Relation
+      transitive-well-founded-relation-Ordinal
+
+  is-asymmetric-le-Ordinal : is-asymmetric le-Ordinal
+  is-asymmetric-le-Ordinal =
+    is-asymmetric-le-Transitive-Well-Founded-Relation
+      transitive-well-founded-relation-Ordinal
+
+  is-irreflexive-le-Ordinal : is-irreflexive le-Ordinal
+  is-irreflexive-le-Ordinal =
+    is-irreflexive-le-Transitive-Well-Founded-Relation
+      transitive-well-founded-relation-Ordinal
+```
+
+The associated reflexive relation on an ordinal.
+
+```agda
+  leq-Ordinal : Relation (l1 ⊔ l2) type-Ordinal
+  leq-Ordinal =
+    leq-Transitive-Well-Founded-Relation
+      transitive-well-founded-relation-Ordinal
+
+  is-prop-leq-Ordinal : {x y : type-Ordinal} → is-prop (leq-Ordinal x y)
+  is-prop-leq-Ordinal {y = y} =
+    is-prop-Π
+      ( λ u →
+        is-prop-function-type (is-prop-type-Relation-Prop le-prop-Ordinal u y))
+
+  leq-prop-Ordinal : Relation-Prop (l1 ⊔ l2) type-Ordinal
+  leq-prop-Ordinal x y = (leq-Ordinal x y , is-prop-leq-Ordinal)
+
+  refl-leq-Ordinal : is-reflexive leq-Ordinal
+  refl-leq-Ordinal =
+    refl-leq-Transitive-Well-Founded-Relation
+      transitive-well-founded-relation-Ordinal
+
+  transitive-leq-Ordinal : is-transitive leq-Ordinal
+  transitive-leq-Ordinal =
+    transitive-leq-Transitive-Well-Founded-Relation
+      transitive-well-founded-relation-Ordinal
+
+  antisymmetric-leq-Ordinal : is-antisymmetric leq-Ordinal
+  antisymmetric-leq-Ordinal x y p q =
+    is-extensional-Ordinal x y (λ u → p u , q u)
+
+  is-preorder-leq-Ordinal : is-preorder-Relation-Prop leq-prop-Ordinal
+  is-preorder-leq-Ordinal = (refl-leq-Ordinal , transitive-leq-Ordinal)
+
+  preorder-Ordinal : Preorder l1 (l1 ⊔ l2)
+  preorder-Ordinal = (type-Ordinal , leq-prop-Ordinal , is-preorder-leq-Ordinal)
+
+  poset-Ordinal : Poset l1 (l1 ⊔ l2)
+  poset-Ordinal = (preorder-Ordinal , antisymmetric-leq-Ordinal)
+
+  is-set-type-Ordinal : is-set type-Ordinal
+  is-set-type-Ordinal = is-set-type-Poset poset-Ordinal
+
+  set-Ordinal : Set l1
+  set-Ordinal = (type-Ordinal , is-set-type-Ordinal)
 ```
diff --git a/src/order-theory/preorders.lagda.md b/src/order-theory/preorders.lagda.md
index f7ac6b21ab..37293a7863 100644
--- a/src/order-theory/preorders.lagda.md
+++ b/src/order-theory/preorders.lagda.md
@@ -30,17 +30,23 @@ open import foundation.universe-levels
 A **preorder** is a type equipped with a reflexive, transitive relation that is
 valued in propositions.
 
-## Definition
+## Definitions
+
+### The predicate on a propositional relation of being a preorder
+
+```agda
+is-preorder-Relation-Prop :
+  {l1 l2 : Level} {X : UU l1} → Relation-Prop l2 X → UU (l1 ⊔ l2)
+is-preorder-Relation-Prop R =
+  is-reflexive-Relation-Prop R × is-transitive-Relation-Prop R
+```
+
+### The type of preorders
 
 ```agda
 Preorder : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
 Preorder l1 l2 =
-  Σ ( UU l1)
-    ( λ X →
-      Σ ( Relation-Prop l2 X)
-        ( λ R →
-          ( is-reflexive (type-Relation-Prop R)) ×
-          ( is-transitive (type-Relation-Prop R))))
+  Σ (UU l1) (λ X → Σ (Relation-Prop l2 X) (is-preorder-Relation-Prop))
 
 module _
   {l1 l2 : Level} (X : Preorder l1 l2)
diff --git a/src/order-theory/transitive-well-founded-relations.lagda.md b/src/order-theory/transitive-well-founded-relations.lagda.md
new file mode 100644
index 0000000000..f011a6666e
--- /dev/null
+++ b/src/order-theory/transitive-well-founded-relations.lagda.md
@@ -0,0 +1,122 @@
+# Transitive well-founded relations
+
+```agda
+module order-theory.transitive-well-founded-relations where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.binary-relations
+open import foundation.cartesian-product-types
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+
+open import order-theory.well-founded-relations
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "transitive well-founded relation" Agda=Transitive-Well-Founded-Relation}}
+is a [transitive](foundation.binary-relations.md)
+[well-founded relation](order-theory.well-founded-relations.md).
+
+## Definitions
+
+### The predicate of being a transitive well-founded relation
+
+```agda
+module _
+  {l1 l2 : Level} {X : UU l1} (R : Relation l2 X)
+  where
+
+  is-transitive-well-founded-relation-Relation : UU (l1 ⊔ l2)
+  is-transitive-well-founded-relation-Relation =
+    is-well-founded-Relation R × is-transitive R
+```
+
+### Transitive well-founded relations
+
+```agda
+Transitive-Well-Founded-Relation :
+  {l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2)
+Transitive-Well-Founded-Relation l2 X =
+  Σ (Relation l2 X) is-transitive-well-founded-relation-Relation
+
+module _
+  {l1 l2 : Level} {X : UU l1} (R : Transitive-Well-Founded-Relation l2 X)
+  where
+
+  le-Transitive-Well-Founded-Relation : Relation l2 X
+  le-Transitive-Well-Founded-Relation = pr1 R
+
+  is-transitive-well-founded-relation-Transitive-Well-Founded-Relation :
+    is-transitive-well-founded-relation-Relation
+      le-Transitive-Well-Founded-Relation
+  is-transitive-well-founded-relation-Transitive-Well-Founded-Relation = pr2 R
+
+  is-well-founded-relation-le-Transitive-Well-Founded-Relation :
+    is-well-founded-Relation le-Transitive-Well-Founded-Relation
+  is-well-founded-relation-le-Transitive-Well-Founded-Relation =
+    pr1 is-transitive-well-founded-relation-Transitive-Well-Founded-Relation
+
+  is-transitive-le-Transitive-Well-Founded-Relation :
+    is-transitive le-Transitive-Well-Founded-Relation
+  is-transitive-le-Transitive-Well-Founded-Relation =
+    pr2 is-transitive-well-founded-relation-Transitive-Well-Founded-Relation
+
+  well-founded-relation-Transitive-Well-Founded-Relation :
+    Well-Founded-Relation l2 X
+  pr1 well-founded-relation-Transitive-Well-Founded-Relation =
+    le-Transitive-Well-Founded-Relation
+  pr2 well-founded-relation-Transitive-Well-Founded-Relation =
+    is-well-founded-relation-le-Transitive-Well-Founded-Relation
+
+  is-asymmetric-le-Transitive-Well-Founded-Relation :
+    is-asymmetric le-Transitive-Well-Founded-Relation
+  is-asymmetric-le-Transitive-Well-Founded-Relation =
+    is-asymmetric-le-Well-Founded-Relation
+      ( well-founded-relation-Transitive-Well-Founded-Relation)
+
+  is-irreflexive-le-Transitive-Well-Founded-Relation :
+    is-irreflexive le-Transitive-Well-Founded-Relation
+  is-irreflexive-le-Transitive-Well-Founded-Relation =
+    is-irreflexive-le-Well-Founded-Relation
+      ( well-founded-relation-Transitive-Well-Founded-Relation)
+```
+
+### The associated reflexive relation of a transitive well-founded relation
+
+Given a transitive well-founded relation `P` there is an associated reflexive
+relation given by
+
+$$
+  (x ≤ y) := (u : X) → u ∈ x → u ∈ y.
+$$
+
+```agda
+module _
+  {l1 l2 : Level} {X : UU l1} (R : Transitive-Well-Founded-Relation l2 X)
+  where
+
+  leq-Transitive-Well-Founded-Relation :
+    Relation (l1 ⊔ l2) X
+  leq-Transitive-Well-Founded-Relation =
+    leq-Well-Founded-Relation
+      ( well-founded-relation-Transitive-Well-Founded-Relation R)
+
+  refl-leq-Transitive-Well-Founded-Relation :
+    is-reflexive leq-Transitive-Well-Founded-Relation
+  refl-leq-Transitive-Well-Founded-Relation =
+    refl-leq-Well-Founded-Relation
+      ( well-founded-relation-Transitive-Well-Founded-Relation R)
+
+  transitive-leq-Transitive-Well-Founded-Relation :
+    is-transitive leq-Transitive-Well-Founded-Relation
+  transitive-leq-Transitive-Well-Founded-Relation =
+    transitive-leq-Well-Founded-Relation
+      ( well-founded-relation-Transitive-Well-Founded-Relation R)
+```
diff --git a/src/order-theory/well-founded-orders.lagda.md b/src/order-theory/well-founded-orders.lagda.md
deleted file mode 100644
index d47e42ac1c..0000000000
--- a/src/order-theory/well-founded-orders.lagda.md
+++ /dev/null
@@ -1,80 +0,0 @@
-# Well-founded orders
-
-```agda
-module order-theory.well-founded-orders where
-```
-
-<details><summary>Imports</summary>
-
-```agda
-open import foundation.binary-relations
-open import foundation.cartesian-product-types
-open import foundation.dependent-pair-types
-open import foundation.universe-levels
-
-open import order-theory.well-founded-relations
-```
-
-</details>
-
-## Idea
-
-A **well-founded order** is a [transitive](foundation.binary-relations.md)
-[well-founded relation](order-theory.well-founded-relations.md).
-
-## Definitions
-
-### The predicate of being a well-founded order
-
-```agda
-module _
-  {l1 l2 : Level} {X : UU l1} (R : Relation l2 X)
-  where
-
-  is-well-founded-order-Relation : UU (l1 ⊔ l2)
-  is-well-founded-order-Relation = is-transitive R × is-well-founded-Relation R
-```
-
-### Well-founded orders
-
-```agda
-Well-Founded-Order : {l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2)
-Well-Founded-Order l2 X = Σ (Relation l2 X) is-well-founded-order-Relation
-
-module _
-  {l1 l2 : Level} {X : UU l1} (R : Well-Founded-Order l2 X)
-  where
-
-  rel-Well-Founded-Order : Relation l2 X
-  rel-Well-Founded-Order = pr1 R
-
-  is-well-founded-order-Well-Founded-Order :
-    is-well-founded-order-Relation rel-Well-Founded-Order
-  is-well-founded-order-Well-Founded-Order = pr2 R
-
-  is-transitive-Well-Founded-Order : is-transitive rel-Well-Founded-Order
-  is-transitive-Well-Founded-Order =
-    pr1 is-well-founded-order-Well-Founded-Order
-
-  is-well-founded-relation-Well-Founded-Order :
-    is-well-founded-Relation rel-Well-Founded-Order
-  is-well-founded-relation-Well-Founded-Order =
-    pr2 is-well-founded-order-Well-Founded-Order
-
-  well-founded-relation-Well-Founded-Order : Well-Founded-Relation l2 X
-  pr1 well-founded-relation-Well-Founded-Order =
-    rel-Well-Founded-Order
-  pr2 well-founded-relation-Well-Founded-Order =
-    is-well-founded-relation-Well-Founded-Order
-
-  is-asymmetric-Well-Founded-Order :
-    is-asymmetric rel-Well-Founded-Order
-  is-asymmetric-Well-Founded-Order =
-    is-asymmetric-Well-Founded-Relation well-founded-relation-Well-Founded-Order
-
-  is-irreflexive-Well-Founded-Order :
-    is-irreflexive rel-Well-Founded-Order
-  is-irreflexive-Well-Founded-Order =
-    is-irreflexive-Well-Founded-Relation
-      ( well-founded-relation-Well-Founded-Order)
-```
diff --git a/src/order-theory/well-founded-relations.lagda.md b/src/order-theory/well-founded-relations.lagda.md
index de06318417..7ae600f45c 100644
--- a/src/order-theory/well-founded-relations.lagda.md
+++ b/src/order-theory/well-founded-relations.lagda.md
@@ -9,10 +9,13 @@ module order-theory.well-founded-relations where
 ```agda
 open import foundation.binary-relations
 open import foundation.dependent-pair-types
+open import foundation.function-types
+open import foundation.identity-types
 open import foundation.propositions
 open import foundation.universe-levels
 
 open import order-theory.accessible-elements-relations
+open import order-theory.preorders
 ```
 
 </details>
@@ -20,18 +23,20 @@ open import order-theory.accessible-elements-relations
 ## Idea
 
 Given a type `X` equipped with a
-[binary relation](foundation.binary-relations.md) `_ϵ_ : X → X → Type` we say
-that the relation `_ϵ_` is **well-founded** if all elements of `X` are
+[binary relation](foundation.binary-relations.md) `_∈_ : X → X → Type` we say
+that the relation `_∈_` is
+{{#concept "well-founded" Disambiguation="binary relation" WDID=Q338021 WD="well-founded relation" Agda=is-well-founded-Relation Agda=Well-Founded-Relation}}
+if all elements of `X` are
 [accessible](order-theory.accessible-elements-relations.md) with respect to
-`_ϵ_`.
+`_∈_`.
 
 Well-founded relations satisfy an induction principle: In order to construct an
 element of `P x` for all `x : X` it suffices to construct an element of `P y`
-for all elements `y ϵ x`. More precisely, the **well-founded induction
+for all elements `y ∈ x`. More precisely, the **well-founded induction
 principle** is a function
 
 ```text
-  (x : X) → ((y : Y) → y ϵ x → P y) → P x.
+  (x : X) → ((y : Y) → y ∈ x → P y) → P x.
 ```
 
 ## Definitions
@@ -40,15 +45,15 @@ principle** is a function
 
 ```agda
 module _
-  {l1 l2 : Level} {X : UU l1} (_ϵ_ : Relation l2 X)
+  {l1 l2 : Level} {X : UU l1} (_∈_ : Relation l2 X)
   where
 
   is-well-founded-prop-Relation : Prop (l1 ⊔ l2)
   is-well-founded-prop-Relation =
-    Π-Prop X (is-accessible-element-prop-Relation _ϵ_)
+    Π-Prop X (is-accessible-element-prop-Relation _∈_)
 
   is-well-founded-Relation : UU (l1 ⊔ l2)
-  is-well-founded-Relation = (x : X) → is-accessible-element-Relation _ϵ_ x
+  is-well-founded-Relation = (x : X) → is-accessible-element-Relation _∈_ x
 ```
 
 ### Well-founded relations
@@ -69,42 +74,74 @@ module _
   is-well-founded-Well-Founded-Relation = pr2 R
 ```
 
-## Properties
-
 ### Well-founded induction
 
 ```agda
 module _
-  {l1 l2 l3 : Level} {X : UU l1} ((_ϵ_ , w) : Well-Founded-Relation l2 X)
+  {l1 l2 l3 : Level} {X : UU l1} ((_∈_ , w) : Well-Founded-Relation l2 X)
   (P : X → UU l3)
   where
 
   ind-Well-Founded-Relation :
-    ({x : X} → ({y : X} → y ϵ x → P y) → P x) → (x : X) → P x
+    ({x : X} → ({y : X} → y ∈ x → P y) → P x) → (x : X) → P x
   ind-Well-Founded-Relation IH x =
-    ind-accessible-element-Relation _ϵ_ P (λ _ → IH) (w x)
+    ind-accessible-element-Relation _∈_ P (λ _ → IH) (w x)
 ```
 
-### A well-founded relation is asymmetric (and thus irreflexive)
+## Properties
+
+### A well-founded relation is asymmetric, and thus irreflexive
 
 ```agda
 module _
-  {l1 l2 : Level} {X : UU l1} ((_ϵ_ , w) : Well-Founded-Relation l2 X)
+  {l1 l2 : Level} {X : UU l1} ((_∈_ , w) : Well-Founded-Relation l2 X)
   where
 
-  is-asymmetric-Well-Founded-Relation :
-    is-asymmetric _ϵ_
-  is-asymmetric-Well-Founded-Relation x y =
-    is-asymmetric-is-accessible-element-Relation _ϵ_ (w x)
+  is-asymmetric-le-Well-Founded-Relation : is-asymmetric _∈_
+  is-asymmetric-le-Well-Founded-Relation x y =
+    is-asymmetric-is-accessible-element-Relation _∈_ (w x)
 
 module _
-  {l1 l2 : Level} {X : UU l1} (ϵ : Well-Founded-Relation l2 X)
+  {l1 l2 : Level} {X : UU l1} (R : Well-Founded-Relation l2 X)
   where
 
-  is-irreflexive-Well-Founded-Relation :
-    is-irreflexive (rel-Well-Founded-Relation ϵ)
-  is-irreflexive-Well-Founded-Relation =
+  is-irreflexive-le-Well-Founded-Relation :
+    is-irreflexive (rel-Well-Founded-Relation R)
+  is-irreflexive-le-Well-Founded-Relation =
     is-irreflexive-is-asymmetric
-      ( rel-Well-Founded-Relation ϵ)
-      ( is-asymmetric-Well-Founded-Relation ϵ)
+      ( rel-Well-Founded-Relation R)
+      ( is-asymmetric-le-Well-Founded-Relation R)
 ```
+
+### The associated reflexive relation of a well-founded relation
+
+Given a well-founded relation `R` on `X` there is an associated reflexive
+relation given by
+
+$$
+  (x ≤ y) := (u : X) → u ∈ x → u ∈ y.
+$$
+
+```agda
+module _
+  {l1 l2 : Level} {X : UU l1} (R@(_∈_ , w) : Well-Founded-Relation l2 X)
+  where
+
+  leq-Well-Founded-Relation : Relation (l1 ⊔ l2) X
+  leq-Well-Founded-Relation x y = (u : X) → u ∈ x → u ∈ y
+
+  refl-leq-Well-Founded-Relation : is-reflexive leq-Well-Founded-Relation
+  refl-leq-Well-Founded-Relation x u = id
+
+  leq-eq-Well-Founded-Relation :
+    {x y : X} → x ＝ y → leq-Well-Founded-Relation x y
+  leq-eq-Well-Founded-Relation {x} refl = refl-leq-Well-Founded-Relation x
+
+  transitive-leq-Well-Founded-Relation : is-transitive leq-Well-Founded-Relation
+  transitive-leq-Well-Founded-Relation x y z f g t H = f t (g t H)
+```
+
+## See also
+
+- A well-founded relation that is transitive is a
+  [transitive well-founded relation](order-theory.transitive-well-founded-relations.md).
diff --git a/src/trees/directed-trees.lagda.md b/src/trees/directed-trees.lagda.md
index 0198184e27..5c60f5b264 100644
--- a/src/trees/directed-trees.lagda.md
+++ b/src/trees/directed-trees.lagda.md
@@ -41,7 +41,7 @@ open import graph-theory.walks-directed-graphs
 
 ## Idea
 
-A **directed tree** is a directed graph `G` equipped with a rood `r : G` such
+A **directed tree** is a directed graph `G` equipped with a root `r : G` such
 that for every vertex `x : G` the type of walks from `x` to `r` is contractible.
 
 ## Definition
diff --git a/theme/index.hbs b/theme/index.hbs
index 44975ea210..49c106f475 100644
--- a/theme/index.hbs
+++ b/theme/index.hbs
@@ -356,6 +356,11 @@
 
     </div>
 
+    <script>
+        window.goatcounter = {
+            path: location.pathname || '/'
+        };
+    </script>
     <script data-goatcounter="https://agda-unimath.goatcounter.com/count" async src="//gc.zgo.at/count.js"></script>
 </body>