diff --git a/references.bib b/references.bib
index d709f0c64f..33606e9ae6 100644
--- a/references.bib
+++ b/references.bib
@@ -28,6 +28,22 @@ @article{AKS15
   langid      = {english}
 }
 
+@article{AL19,
+  title       = {Displayed Categories},
+  author      = {Ahrens, Benedikt and {{LeFanu}} Lumsdaine, Peter},
+  doi         = {10.23638/LMCS-15(1:20)2019},
+  journal     = {{Logical Methods in Computer Science}},
+  volume      = {15},
+  issue       = {1},
+  year        = {2019},
+  month       = {03},
+  keywords    = {Mathematics - Category Theory ; Mathematics - Logic ; 18A15, 03B15, 03B70 ; F.4.1},
+  eprint      = {1705.04296},
+  eprinttype  = {arxiv},
+  eprintclass = {math},
+  langid      = {english}
+}
+
 @online{BCDE21,
   title  = {Free groups in HoTT/UF in Agda},
   author = {Bezem, Marc and Coquand, Thierry and Dybjer, Peter and Escardó, Martín},
diff --git a/src/category-theory.lagda.md b/src/category-theory.lagda.md
index e4bb19aab7..4e0084b390 100644
--- a/src/category-theory.lagda.md
+++ b/src/category-theory.lagda.md
@@ -38,11 +38,13 @@ open import category-theory.coproducts-in-precategories public
 open import category-theory.cores-categories public
 open import category-theory.cores-precategories public
 open import category-theory.coslice-precategories public
+open import category-theory.dependent-composition-operations-over-precategories public
 open import category-theory.dependent-products-of-categories public
 open import category-theory.dependent-products-of-large-categories public
 open import category-theory.dependent-products-of-large-precategories public
 open import category-theory.dependent-products-of-precategories public
 open import category-theory.discrete-categories public
+open import category-theory.displayed-precategories public
 open import category-theory.embedding-maps-precategories public
 open import category-theory.embeddings-precategories public
 open import category-theory.endomorphisms-in-categories public
diff --git a/src/category-theory/dependent-composition-operations-over-precategories.lagda.md b/src/category-theory/dependent-composition-operations-over-precategories.lagda.md
new file mode 100644
index 0000000000..8f663b706e
--- /dev/null
+++ b/src/category-theory/dependent-composition-operations-over-precategories.lagda.md
@@ -0,0 +1,269 @@
+# Dependent composition operations over precategories
+
+```agda
+module category-theory.dependent-composition-operations-over-precategories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.composition-operations-on-binary-families-of-sets
+open import category-theory.nonunital-precategories
+open import category-theory.precategories
+open import category-theory.set-magmoids
+
+open import foundation.cartesian-product-types
+open import foundation.dependent-identifications
+open import foundation.dependent-pair-types
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.iterated-dependent-product-types
+open import foundation.propositions
+open import foundation.sets
+open import foundation.transport-along-identifications
+open import foundation.truncated-types
+open import foundation.truncation-levels
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+Given a [precategory](category-theory.precategories.md) `C`, a
+{{#concept "dependent composition structure" Disambiguation="over a precategory"}}
+`D` over `C` is a family of types `obj D` over `obj C` and a family of
+_hom-[sets](foundation-core.sets.md)_
+
+```text
+hom D : hom C x y → obj D x → obj D y → Set
+```
+
+for every pair `x y : obj C`, equipped with a
+{{#concept "dependent composition operation" Disambiguation="over a precategory" Agda=dependent-composition-operation-Precategory}}
+
+```text
+  comp D : hom D g y' z' → hom D f x' y' → hom D (g ∘ f) x' z'.
+```
+
+## Definitions
+
+### The type of dependent composition operations over a precategory
+
+```agda
+module _
+  {l1 l2 : Level} (C : Precategory l1 l2)
+  where
+
+  dependent-composition-operation-Precategory :
+    { l3 l4 : Level}
+    ( obj-D : obj-Precategory C → UU l3) →
+    ( hom-set-D :
+      {x y : obj-Precategory C}
+      (f : hom-Precategory C x y)
+      (x' : obj-D x) (y' : obj-D y) → Set l4) →
+      UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  dependent-composition-operation-Precategory obj-D hom-set-D =
+    {x y z : obj-Precategory C}
+    (g : hom-Precategory C y z) (f : hom-Precategory C x y) →
+    {x' : obj-D x} {y' : obj-D y} {z' : obj-D z} →
+    (g' : type-Set (hom-set-D g y' z')) (f' : type-Set (hom-set-D f x' y')) →
+    type-Set (hom-set-D (comp-hom-Precategory C g f) x' z')
+```
+
+### The predicate of being associative on dependent composition operations over a precategory
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (C : Precategory l1 l2)
+  ( obj-D : obj-Precategory C → UU l3)
+  ( hom-set-D :
+    {x y : obj-Precategory C}
+    (f : hom-Precategory C x y) (x' : obj-D x) (y' : obj-D y) → Set l4)
+  ( comp-hom-D : dependent-composition-operation-Precategory C obj-D hom-set-D)
+  where
+
+  is-associative-dependent-composition-operation-Precategory :
+    UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-associative-dependent-composition-operation-Precategory =
+    {x y z w : obj-Precategory C}
+    (h : hom-Precategory C z w)
+    (g : hom-Precategory C y z)
+    (f : hom-Precategory C x y)
+    {x' : obj-D x} {y' : obj-D y} {z' : obj-D z} {w' : obj-D w}
+    (h' : type-Set (hom-set-D h z' w'))
+    (g' : type-Set (hom-set-D g y' z'))
+    (f' : type-Set (hom-set-D f x' y')) →
+    dependent-identification
+      ( λ i → type-Set (hom-set-D i x' w'))
+      ( associative-comp-hom-Precategory C h g f)
+      ( comp-hom-D (comp-hom-Precategory C h g) f (comp-hom-D h g h' g') f')
+      ( comp-hom-D h (comp-hom-Precategory C g f) h' (comp-hom-D g f g' f'))
+
+  is-prop-is-associative-dependent-composition-operation-Precategory :
+    is-prop is-associative-dependent-composition-operation-Precategory
+  is-prop-is-associative-dependent-composition-operation-Precategory =
+    is-prop-iterated-implicit-Π 4
+      ( λ x y z w →
+        is-prop-iterated-Π 3
+          ( λ h g f →
+            is-prop-iterated-implicit-Π 4
+              ( λ x' y' z' w' →
+                is-prop-iterated-Π 3
+                  ( λ h' g' f' →
+                    is-set-type-Set
+                      ( hom-set-D
+                        ( comp-hom-Precategory C h (comp-hom-Precategory C g f))
+                        ( x')
+                        ( w'))
+                      ( tr
+                        ( λ i → type-Set (hom-set-D i x' w'))
+                        ( associative-comp-hom-Precategory C h g f)
+                        ( comp-hom-D
+                          ( comp-hom-Precategory C h g)
+                          ( f)
+                          ( comp-hom-D h g h' g')
+                          ( f')))
+                      ( comp-hom-D
+                        ( h)
+                        ( comp-hom-Precategory C g f)
+                        ( h')
+                        ( comp-hom-D g f g' f'))))))
+
+  is-associative-prop-dependent-composition-operation-Precategory :
+    Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  pr1 is-associative-prop-dependent-composition-operation-Precategory =
+    is-associative-dependent-composition-operation-Precategory
+  pr2 is-associative-prop-dependent-composition-operation-Precategory =
+    is-prop-is-associative-dependent-composition-operation-Precategory
+```
+
+### The predicate of being unital on dependent composition operations over a precategory
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (C : Precategory l1 l2)
+  ( obj-D : obj-Precategory C → UU l3)
+  ( hom-set-D :
+    {x y : obj-Precategory C}
+    (f : hom-Precategory C x y) (x' : obj-D x) (y' : obj-D y) → Set l4)
+  ( comp-hom-D : dependent-composition-operation-Precategory C obj-D hom-set-D)
+  ( id-hom-D :
+    {x : obj-Precategory C} (x' : obj-D x) →
+    type-Set (hom-set-D (id-hom-Precategory C {x}) x' x'))
+  where
+
+  is-left-unit-dependent-composition-operation-Precategory :
+    UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-left-unit-dependent-composition-operation-Precategory =
+    {x y : obj-Precategory C} (f : hom-Precategory C x y)
+    {x' : obj-D x} {y' : obj-D y} (f' : type-Set (hom-set-D f x' y')) →
+    dependent-identification
+      ( λ i → type-Set (hom-set-D i x' y'))
+      ( left-unit-law-comp-hom-Precategory C f)
+      ( comp-hom-D (id-hom-Precategory C) f (id-hom-D y') f')
+      ( f')
+
+  is-prop-is-left-unit-dependent-composition-operation-Precategory :
+    is-prop is-left-unit-dependent-composition-operation-Precategory
+  is-prop-is-left-unit-dependent-composition-operation-Precategory =
+    is-prop-iterated-implicit-Π 2
+      ( λ x y →
+        is-prop-Π
+          ( λ f →
+            is-prop-iterated-implicit-Π 2
+              ( λ x' y' →
+                is-prop-Π
+                  ( λ f' →
+                    is-set-type-Set
+                      ( hom-set-D f x' y')
+                      ( tr
+                        ( λ i → type-Set (hom-set-D i x' y'))
+                        ( left-unit-law-comp-hom-Precategory C f)
+                        ( comp-hom-D (id-hom-Precategory C) f (id-hom-D y') f'))
+                      ( f')))))
+
+  is-left-unit-prop-dependent-composition-operation-Precategory :
+    Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  pr1 is-left-unit-prop-dependent-composition-operation-Precategory =
+    is-left-unit-dependent-composition-operation-Precategory
+  pr2 is-left-unit-prop-dependent-composition-operation-Precategory =
+    is-prop-is-left-unit-dependent-composition-operation-Precategory
+
+  is-right-unit-dependent-composition-operation-Precategory :
+    UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-right-unit-dependent-composition-operation-Precategory =
+    {x y : obj-Precategory C} (f : hom-Precategory C x y)
+    {x' : obj-D x} {y' : obj-D y} (f' : type-Set (hom-set-D f x' y')) →
+    dependent-identification
+      ( λ i → type-Set (hom-set-D i x' y'))
+      ( right-unit-law-comp-hom-Precategory C f)
+      ( comp-hom-D f (id-hom-Precategory C) f' (id-hom-D x'))
+      ( f')
+
+  is-prop-is-right-unit-dependent-composition-operation-Precategory :
+    is-prop is-right-unit-dependent-composition-operation-Precategory
+  is-prop-is-right-unit-dependent-composition-operation-Precategory =
+    is-prop-iterated-implicit-Π 2
+      ( λ x y →
+        is-prop-Π
+          ( λ f →
+            is-prop-iterated-implicit-Π 2
+              ( λ x' y' →
+                is-prop-Π
+                  ( λ f' →
+                    is-set-type-Set
+                      ( hom-set-D f x' y')
+                      ( tr
+                        ( λ i → type-Set (hom-set-D i x' y'))
+                        ( right-unit-law-comp-hom-Precategory C f)
+                        ( comp-hom-D f (id-hom-Precategory C) f' (id-hom-D x')))
+                      ( f')))))
+
+  is-right-unit-prop-dependent-composition-operation-Precategory :
+    Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  pr1 is-right-unit-prop-dependent-composition-operation-Precategory =
+    is-right-unit-dependent-composition-operation-Precategory
+  pr2 is-right-unit-prop-dependent-composition-operation-Precategory =
+    is-prop-is-right-unit-dependent-composition-operation-Precategory
+
+  is-unit-dependent-composition-operation-Precategory :
+    UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-unit-dependent-composition-operation-Precategory =
+    ( is-left-unit-dependent-composition-operation-Precategory) ×
+    ( is-right-unit-dependent-composition-operation-Precategory)
+
+  is-prop-is-unit-dependent-composition-operation-Precategory :
+    is-prop is-unit-dependent-composition-operation-Precategory
+  is-prop-is-unit-dependent-composition-operation-Precategory =
+    is-prop-product
+      ( is-prop-is-left-unit-dependent-composition-operation-Precategory)
+      ( is-prop-is-right-unit-dependent-composition-operation-Precategory)
+
+  is-unit-prop-dependent-composition-operation-Precategory :
+    Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  pr1 is-unit-prop-dependent-composition-operation-Precategory =
+    is-unit-dependent-composition-operation-Precategory
+  pr2 is-unit-prop-dependent-composition-operation-Precategory =
+    is-prop-is-unit-dependent-composition-operation-Precategory
+
+module _
+  {l1 l2 l3 l4 : Level} (C : Precategory l1 l2)
+  ( obj-D : obj-Precategory C → UU l3)
+  ( hom-set-D :
+    {x y : obj-Precategory C}
+    (f : hom-Precategory C x y) (x' : obj-D x) (y' : obj-D y) → Set l4)
+  ( comp-hom-D : dependent-composition-operation-Precategory C obj-D hom-set-D)
+  where
+
+  is-unital-dependent-composition-operation-Precategory : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-unital-dependent-composition-operation-Precategory =
+    Σ ( {x : obj-Precategory C} (x' : obj-D x) →
+        type-Set (hom-set-D (id-hom-Precategory C {x}) x' x'))
+      ( is-unit-dependent-composition-operation-Precategory C
+          obj-D hom-set-D comp-hom-D)
+```
+
+## See also
+
+- [Displayed precategories](category-theory.displayed-precategories.md)
diff --git a/src/category-theory/displayed-precategories.lagda.md b/src/category-theory/displayed-precategories.lagda.md
new file mode 100644
index 0000000000..959ce0871a
--- /dev/null
+++ b/src/category-theory/displayed-precategories.lagda.md
@@ -0,0 +1,470 @@
+# Displayed precategories
+
+```agda
+module category-theory.displayed-precategories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.composition-operations-on-binary-families-of-sets
+open import category-theory.dependent-composition-operations-over-precategories
+open import category-theory.nonunital-precategories
+open import category-theory.precategories
+open import category-theory.set-magmoids
+
+open import foundation.cartesian-product-types
+open import foundation.dependent-identifications
+open import foundation.dependent-pair-types
+open import foundation.equality-dependent-pair-types
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.iterated-dependent-product-types
+open import foundation.propositions
+open import foundation.sets
+open import foundation.strictly-involutive-identity-types
+open import foundation.subsingleton-induction
+open import foundation.transport-along-identifications
+open import foundation.truncated-types
+open import foundation.truncation-levels
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+Given a [precategory](category-theory.precategories.md) `𝒞`, a
+{{#concept "displayed precategory" Agda=Displayed-Precategory}} over `𝒞` is an
+associative and unital
+[dependent composition structure](category-theory.dependent-composition-operations-over-precategories.md)
+over it.
+
+Thus, a displayed precategory `𝒟` over `𝒞` consists of
+
+- a family of objects `obj 𝒟` indexed by `obj 𝒞`,
+- a family of hom-[sets](foundation-core.sets.md)
+
+  ```text
+  hom 𝒟 : hom 𝒞 x y → obj 𝒟 x → obj 𝒟 y → Set,
+  ```
+
+  for every pair `x y : obj 𝒞`, and
+
+- a dependent composition operation
+
+  ```text
+    comp 𝒟 : hom 𝒟 g y' z' → hom 𝒟 f x' y' → hom 𝒟 (g ∘ f) x' z'
+  ```
+
+  such that
+
+- The dependent associativity condition
+
+  ```text
+  comp 𝒟 (comp 𝒟 h' g') f' ＝ comp 𝒟 h' (comp 𝒟 g' f')
+  ```
+
+  over the associativity witness `(h ∘ g) ∘ f ＝ h ∘ (g ∘ f)` in `𝒞` holds, and
+
+- the composition operation is dependent unital, meaning there is a family of
+  identity morphisms
+
+  ```text
+    id 𝒟 : (x : obj 𝒞) (x' : obj 𝒟 x) → hom 𝒟 (id 𝒞 x) x' x'
+  ```
+
+  which is a dependent left and right unit in the sense that the dependent
+  identities `comp 𝒟 (id 𝒟) f ＝ f` and `comp 𝒟 f (id 𝒟) ＝ f` hold over the
+  respective witnesses of left and right unitality in `𝒞`.
+
+## Definitions
+
+### The predicate of being a displayed precategory
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (𝒞 : Precategory l1 l2)
+  ( obj-𝒟 : obj-Precategory 𝒞 → UU l3)
+  ( hom-set-𝒟 :
+    {x y : obj-Precategory 𝒞}
+    (f : hom-Precategory 𝒞 x y) (x' : obj-𝒟 x) (y' : obj-𝒟 y) → Set l4)
+  ( comp-hom-𝒟 : dependent-composition-operation-Precategory 𝒞 obj-𝒟 hom-set-𝒟)
+  where
+
+  is-displayed-precategory : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-displayed-precategory =
+    ( is-associative-dependent-composition-operation-Precategory 𝒞
+        obj-𝒟 hom-set-𝒟 comp-hom-𝒟) ×
+    ( is-unital-dependent-composition-operation-Precategory 𝒞
+        obj-𝒟 hom-set-𝒟 comp-hom-𝒟)
+```
+
+### The type of displayed precategories over a precategory
+
+```agda
+module _
+  {l1 l2 : Level} (l3 l4 : Level) (𝒞 : Precategory l1 l2)
+  where
+
+  Displayed-Precategory : UU (l1 ⊔ l2 ⊔ lsuc l3 ⊔ lsuc l4)
+  Displayed-Precategory =
+    Σ ( obj-Precategory 𝒞 → UU l3)
+      ( λ obj-𝒟 →
+        Σ ( {x y : obj-Precategory 𝒞}
+            (f : hom-Precategory 𝒞 x y) (x' : obj-𝒟 x) (y' : obj-𝒟 y) → Set l4)
+          ( λ hom-set-𝒟 →
+            Σ ( dependent-composition-operation-Precategory 𝒞 obj-𝒟 hom-set-𝒟)
+              ( is-displayed-precategory 𝒞 obj-𝒟 hom-set-𝒟)))
+
+module _
+  {l1 l2 l3 l4 : Level}
+  (𝒞 : Precategory l1 l2) (𝒟 : Displayed-Precategory l3 l4 𝒞)
+  where
+
+  obj-Displayed-Precategory : obj-Precategory 𝒞 → UU l3
+  obj-Displayed-Precategory = pr1 𝒟
+
+  hom-set-Displayed-Precategory :
+    {x y : obj-Precategory 𝒞} (f : hom-Precategory 𝒞 x y)
+    (x' : obj-Displayed-Precategory x) (y' : obj-Displayed-Precategory y) →
+    Set l4
+  hom-set-Displayed-Precategory = pr1 (pr2 𝒟)
+
+  hom-Displayed-Precategory :
+    {x y : obj-Precategory 𝒞} (f : hom-Precategory 𝒞 x y)
+    (x' : obj-Displayed-Precategory x) (y' : obj-Displayed-Precategory y) →
+    UU l4
+  hom-Displayed-Precategory f x' y' =
+    type-Set (hom-set-Displayed-Precategory f x' y')
+
+  is-set-hom-Displayed-Precategory :
+    {x y : obj-Precategory 𝒞} (f : hom-Precategory 𝒞 x y)
+    (x' : obj-Displayed-Precategory x) (y' : obj-Displayed-Precategory y) →
+    is-set (hom-Displayed-Precategory f x' y')
+  is-set-hom-Displayed-Precategory f x' y' =
+    is-set-type-Set (hom-set-Displayed-Precategory f x' y')
+
+  comp-hom-Displayed-Precategory :
+    dependent-composition-operation-Precategory 𝒞
+      ( obj-Displayed-Precategory)
+      ( hom-set-Displayed-Precategory)
+  comp-hom-Displayed-Precategory = pr1 (pr2 (pr2 𝒟))
+
+  associative-comp-hom-Displayed-Precategory :
+    is-associative-dependent-composition-operation-Precategory 𝒞
+      ( obj-Displayed-Precategory)
+      ( hom-set-Displayed-Precategory)
+      ( comp-hom-Displayed-Precategory)
+  associative-comp-hom-Displayed-Precategory = pr1 (pr2 (pr2 (pr2 𝒟)))
+
+  is-unital-comp-hom-Displayed-Precategory :
+    is-unital-dependent-composition-operation-Precategory 𝒞
+      ( obj-Displayed-Precategory)
+      ( hom-set-Displayed-Precategory)
+      ( comp-hom-Displayed-Precategory)
+  is-unital-comp-hom-Displayed-Precategory = pr2 (pr2 (pr2 (pr2 𝒟)))
+
+  id-hom-Displayed-Precategory :
+    {x : obj-Precategory 𝒞} (x' : obj-Displayed-Precategory x) →
+    hom-Displayed-Precategory (id-hom-Precategory 𝒞) x' x'
+  id-hom-Displayed-Precategory = pr1 is-unital-comp-hom-Displayed-Precategory
+
+  left-unit-law-comp-hom-Displayed-Precategory :
+    is-left-unit-dependent-composition-operation-Precategory 𝒞
+      obj-Displayed-Precategory
+      hom-set-Displayed-Precategory
+      comp-hom-Displayed-Precategory
+      id-hom-Displayed-Precategory
+  left-unit-law-comp-hom-Displayed-Precategory =
+    pr1 (pr2 is-unital-comp-hom-Displayed-Precategory)
+
+  right-unit-law-comp-hom-Displayed-Precategory :
+    is-right-unit-dependent-composition-operation-Precategory 𝒞
+      obj-Displayed-Precategory
+      hom-set-Displayed-Precategory
+      comp-hom-Displayed-Precategory
+      id-hom-Displayed-Precategory
+  right-unit-law-comp-hom-Displayed-Precategory =
+    pr2 (pr2 is-unital-comp-hom-Displayed-Precategory)
+```
+
+### The total precategory associated to a displayed precategory
+
+Given a displayed precategory `𝒟` over `𝒞`, the total structure `∫D` whose
+objects are
+
+```text
+  obj ∫D := Σ (x : obj 𝒞) (obj 𝒟 x)
+```
+
+and hom-sets are
+
+```text
+  hom ∫D (x , x') (y , y') := Σ (f : hom 𝒞 x y) (hom 𝒟 f x' y')
+```
+
+form a precategory called the
+{{#concept "total precategory" Disambiguation="of a displayed precategory" Agda=total-precategory-Displayed-Precategory}}
+of `𝒟`.
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (𝒞 : Precategory l1 l2) (𝒟 : Displayed-Precategory l3 l4 𝒞)
+  where
+
+  obj-total-precategory-Displayed-Precategory : UU (l1 ⊔ l3)
+  obj-total-precategory-Displayed-Precategory =
+    Σ (obj-Precategory 𝒞) (obj-Displayed-Precategory 𝒞 𝒟)
+
+  hom-set-total-precategory-Displayed-Precategory :
+    (x y : obj-total-precategory-Displayed-Precategory) → Set (l2 ⊔ l4)
+  hom-set-total-precategory-Displayed-Precategory (x , x') (y , y') =
+    Σ-Set
+      ( hom-set-Precategory 𝒞 x y)
+      ( λ f → hom-set-Displayed-Precategory 𝒞 𝒟 f x' y')
+
+  hom-total-precategory-Displayed-Precategory :
+    (x y : obj-total-precategory-Displayed-Precategory) → UU (l2 ⊔ l4)
+  hom-total-precategory-Displayed-Precategory x y =
+    type-Set (hom-set-total-precategory-Displayed-Precategory x y)
+
+  comp-hom-total-precategory-Displayed-Precategory :
+    {x y z : obj-total-precategory-Displayed-Precategory} →
+    hom-total-precategory-Displayed-Precategory y z →
+    hom-total-precategory-Displayed-Precategory x y →
+    hom-total-precategory-Displayed-Precategory x z
+  pr1 (comp-hom-total-precategory-Displayed-Precategory (g , g') (f , f')) =
+    comp-hom-Precategory 𝒞 g f
+  pr2 (comp-hom-total-precategory-Displayed-Precategory (g , g') (f , f')) =
+    comp-hom-Displayed-Precategory 𝒞 𝒟 g f g' f'
+
+  associative-comp-hom-total-precategory-Displayed-Precategory :
+    {x y z w : obj-total-precategory-Displayed-Precategory}
+    (h : hom-total-precategory-Displayed-Precategory z w)
+    (g : hom-total-precategory-Displayed-Precategory y z)
+    (f : hom-total-precategory-Displayed-Precategory x y) →
+    ( comp-hom-total-precategory-Displayed-Precategory
+      ( comp-hom-total-precategory-Displayed-Precategory h g)
+      ( f)) ＝
+    ( comp-hom-total-precategory-Displayed-Precategory
+      ( h)
+      ( comp-hom-total-precategory-Displayed-Precategory g f))
+  associative-comp-hom-total-precategory-Displayed-Precategory
+    ( h , h') (g , g') (f , f') =
+    eq-pair-Σ
+      ( associative-comp-hom-Precategory 𝒞 h g f)
+      ( associative-comp-hom-Displayed-Precategory 𝒞 𝒟 h g f h' g' f')
+
+  associative-composition-operation-total-precategory-Displayed-Precategory :
+    associative-composition-operation-binary-family-Set
+      ( hom-set-total-precategory-Displayed-Precategory)
+  associative-composition-operation-total-precategory-Displayed-Precategory =
+    ( comp-hom-total-precategory-Displayed-Precategory) ,
+    ( λ h g f →
+      involutive-eq-eq
+        ( associative-comp-hom-total-precategory-Displayed-Precategory h g f))
+
+  id-hom-total-precategory-Displayed-Precategory :
+    {x : obj-total-precategory-Displayed-Precategory} →
+    hom-total-precategory-Displayed-Precategory x x
+  pr1 (id-hom-total-precategory-Displayed-Precategory {x , x'}) =
+    id-hom-Precategory 𝒞
+  pr2 (id-hom-total-precategory-Displayed-Precategory {x , x'}) =
+    id-hom-Displayed-Precategory 𝒞 𝒟 x'
+
+  left-unit-law-comp-hom-total-precategory-Displayed-Precategory :
+    {x y : obj-total-precategory-Displayed-Precategory} →
+    (f : hom-total-precategory-Displayed-Precategory x y) →
+    comp-hom-total-precategory-Displayed-Precategory
+      ( id-hom-total-precategory-Displayed-Precategory)
+      ( f) ＝
+    f
+  left-unit-law-comp-hom-total-precategory-Displayed-Precategory (f , f') =
+    eq-pair-Σ
+      ( left-unit-law-comp-hom-Precategory 𝒞 f)
+      ( left-unit-law-comp-hom-Displayed-Precategory 𝒞 𝒟 f f')
+
+  right-unit-law-comp-hom-total-precategory-Displayed-Precategory :
+    {x y : obj-total-precategory-Displayed-Precategory} →
+    (f : hom-total-precategory-Displayed-Precategory x y) →
+    comp-hom-total-precategory-Displayed-Precategory
+      ( f)
+      ( id-hom-total-precategory-Displayed-Precategory) ＝
+    f
+  right-unit-law-comp-hom-total-precategory-Displayed-Precategory (f , f') =
+    eq-pair-Σ
+      ( right-unit-law-comp-hom-Precategory 𝒞 f)
+      ( right-unit-law-comp-hom-Displayed-Precategory 𝒞 𝒟 f f')
+
+  is-unital-composition-operation-total-precategory-Displayed-Precategory :
+    is-unital-composition-operation-binary-family-Set
+      ( hom-set-total-precategory-Displayed-Precategory)
+      ( comp-hom-total-precategory-Displayed-Precategory)
+  pr1
+    is-unital-composition-operation-total-precategory-Displayed-Precategory x =
+    id-hom-total-precategory-Displayed-Precategory
+  pr1
+    ( pr2
+      is-unital-composition-operation-total-precategory-Displayed-Precategory) =
+        left-unit-law-comp-hom-total-precategory-Displayed-Precategory
+  pr2
+    ( pr2
+      is-unital-composition-operation-total-precategory-Displayed-Precategory) =
+        right-unit-law-comp-hom-total-precategory-Displayed-Precategory
+
+  total-precategory-Displayed-Precategory : Precategory (l1 ⊔ l3) (l2 ⊔ l4)
+  pr1 total-precategory-Displayed-Precategory =
+    obj-total-precategory-Displayed-Precategory
+  pr1 (pr2 total-precategory-Displayed-Precategory) =
+    hom-set-total-precategory-Displayed-Precategory
+  pr1 (pr2 (pr2 total-precategory-Displayed-Precategory)) =
+    associative-composition-operation-total-precategory-Displayed-Precategory
+  pr2 (pr2 (pr2 total-precategory-Displayed-Precategory)) =
+    is-unital-composition-operation-total-precategory-Displayed-Precategory
+```
+
+### The fiber precategory of a displayed precategory over an object
+
+Given a displayed precategory `𝒟` over `𝒞`, the fiber of `𝒟` over `x : obj 𝒞`
+defines a precategory.
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (𝒞 : Precategory l1 l2) (𝒟 : Displayed-Precategory l3 l4 𝒞)
+  (c : obj-Precategory 𝒞)
+  where
+
+  obj-fiber-precategory-Displayed-Precategory : UU l3
+  obj-fiber-precategory-Displayed-Precategory = obj-Displayed-Precategory 𝒞 𝒟 c
+
+  hom-set-fiber-precategory-Displayed-Precategory :
+    (x y : obj-fiber-precategory-Displayed-Precategory) → Set l4
+  hom-set-fiber-precategory-Displayed-Precategory =
+    hom-set-Displayed-Precategory 𝒞 𝒟 (id-hom-Precategory 𝒞 {c})
+
+  hom-fiber-precategory-Displayed-Precategory :
+    (x y : obj-fiber-precategory-Displayed-Precategory) → UU l4
+  hom-fiber-precategory-Displayed-Precategory x y =
+    type-Set (hom-set-fiber-precategory-Displayed-Precategory x y)
+
+  comp-hom-fiber-precategory-Displayed-Precategory :
+    {x y z : obj-fiber-precategory-Displayed-Precategory} →
+    hom-fiber-precategory-Displayed-Precategory y z →
+    hom-fiber-precategory-Displayed-Precategory x y →
+    hom-fiber-precategory-Displayed-Precategory x z
+  comp-hom-fiber-precategory-Displayed-Precategory {x} {y} {z} g f =
+    tr
+      ( λ i → hom-Displayed-Precategory 𝒞 𝒟 i x z)
+      ( left-unit-law-comp-hom-Precategory 𝒞 (id-hom-Precategory 𝒞))
+      ( comp-hom-Displayed-Precategory 𝒞 𝒟
+        ( id-hom-Precategory 𝒞) (id-hom-Precategory 𝒞) g f)
+```
+
+By associativity in `𝒟`, composition in the fiber is dependently associative
+
+```text
+      f       g       h
+  x ----> y ----> z ----> w
+
+  c ===== c ===== c ===== c
+```
+
+The proof remains to be formalized.
+
+```text
+  associative-comp-hom-fiber-precategory-Displayed-Precategory :
+    {x y z w : obj-fiber-precategory-Displayed-Precategory}
+    (h : hom-fiber-precategory-Displayed-Precategory z w)
+    (g : hom-fiber-precategory-Displayed-Precategory y z)
+    (f : hom-fiber-precategory-Displayed-Precategory x y) →
+    ( comp-hom-fiber-precategory-Displayed-Precategory
+      ( comp-hom-fiber-precategory-Displayed-Precategory h g)
+      ( f)) ＝
+    ( comp-hom-fiber-precategory-Displayed-Precategory
+      ( h)
+      ( comp-hom-fiber-precategory-Displayed-Precategory g f))
+  associative-comp-hom-fiber-precategory-Displayed-Precategory
+    {x} {y} {z} {w} h g f =
+      {! associative-comp-hom-Displayed-Precategory 𝒞 𝒟 _ _ _ h g f  !}
+```
+
+```text
+  associative-composition-operation-fiber-precategory-Displayed-Precategory :
+    associative-composition-operation-binary-family-Set
+      ( hom-set-fiber-precategory-Displayed-Precategory)
+  pr1
+    associative-composition-operation-fiber-precategory-Displayed-Precategory =
+    comp-hom-fiber-precategory-Displayed-Precategory
+  pr2
+    associative-composition-operation-fiber-precategory-Displayed-Precategory =
+    associative-comp-hom-fiber-precategory-Displayed-Precategory
+
+  id-hom-fiber-precategory-Displayed-Precategory :
+    {x : obj-fiber-precategory-Displayed-Precategory} →
+    hom-fiber-precategory-Displayed-Precategory x x
+  id-hom-fiber-precategory-Displayed-Precategory {x} =
+    id-hom-Displayed-Precategory 𝒞 𝒟 x
+
+  left-unit-law-comp-hom-fiber-precategory-Displayed-Precategory :
+    {x y : obj-fiber-precategory-Displayed-Precategory} →
+    (f : hom-fiber-precategory-Displayed-Precategory x y) →
+    comp-hom-fiber-precategory-Displayed-Precategory
+      ( id-hom-fiber-precategory-Displayed-Precategory)
+      ( f) ＝
+    f
+  left-unit-law-comp-hom-fiber-precategory-Displayed-Precategory =
+    left-unit-law-comp-hom-Displayed-Precategory 𝒞 𝒟 (id-hom-Precategory 𝒞 {c})
+
+  right-unit-law-comp-hom-fiber-precategory-Displayed-Precategory :
+    {x y : obj-fiber-precategory-Displayed-Precategory} →
+    (f : hom-fiber-precategory-Displayed-Precategory x y) →
+    comp-hom-fiber-precategory-Displayed-Precategory
+      ( f)
+      ( id-hom-fiber-precategory-Displayed-Precategory) ＝
+    f
+  right-unit-law-comp-hom-fiber-precategory-Displayed-Precategory =
+    right-unit-law-comp-hom-Displayed-Precategory 𝒞 𝒟 (id-hom-Precategory 𝒞 {c})
+
+  is-unital-composition-operation-fiber-precategory-Displayed-Precategory :
+    is-unital-composition-operation-binary-family-Set
+      ( hom-set-fiber-precategory-Displayed-Precategory)
+      ( comp-hom-fiber-precategory-Displayed-Precategory)
+  pr1
+    is-unital-composition-operation-fiber-precategory-Displayed-Precategory x =
+    id-hom-fiber-precategory-Displayed-Precategory
+  pr1
+    ( pr2
+      is-unital-composition-operation-fiber-precategory-Displayed-Precategory) =
+        left-unit-law-comp-hom-fiber-precategory-Displayed-Precategory
+  pr2
+    ( pr2
+      is-unital-composition-operation-fiber-precategory-Displayed-Precategory) =
+        right-unit-law-comp-hom-fiber-precategory-Displayed-Precategory
+
+  fiber-precategory-Displayed-Precategory : Precategory l3 l4
+  pr1 fiber-precategory-Displayed-Precategory =
+    obj-fiber-precategory-Displayed-Precategory
+  pr1 (pr2 fiber-precategory-Displayed-Precategory) =
+    hom-set-fiber-precategory-Displayed-Precategory
+  pr1 (pr2 (pr2 fiber-precategory-Displayed-Precategory)) =
+    associative-composition-operation-fiber-precategory-Displayed-Precategory
+  pr2 (pr2 (pr2 fiber-precategory-Displayed-Precategory)) =
+    is-unital-composition-operation-fiber-precategory-Displayed-Precategory
+```
+
+## References
+
+{{#bibliography}} {{#reference AL19}}
+
+## External links
+
+- [Displayed Categories](https://1lab.dev/Cat.Displayed.Base.html) at 1lab
+- [displayed category](https://ncatlab.org/nlab/show/displayed+category) at
+  $n$Lab
+- [Displayed categories](https://www.epatters.org/wiki/algebra/displayed-categories)
+  at Evan Patterson's blog
+
+A wikidata identifier was not available for this concept.
diff --git a/src/category-theory/precategories.lagda.md b/src/category-theory/precategories.lagda.md
index dc2e72e23a..1eb71cad75 100644
--- a/src/category-theory/precategories.lagda.md
+++ b/src/category-theory/precategories.lagda.md
@@ -11,6 +11,7 @@ open import category-theory.composition-operations-on-binary-families-of-sets
 open import category-theory.nonunital-precategories
 open import category-theory.set-magmoids
 
+open import foundation.action-on-identifications-functions
 open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
 open import foundation.function-types
@@ -316,6 +317,71 @@ module _
       ( nonunital-precategory-Precategory C)
 ```
 
+### Coherence between the left and right unit law of a precategory
+
+```agda
+module _
+  {l1 l2 : Level} (C : Precategory l1 l2)
+  where
+
+  coh-unit-laws-comp-hom-Precategory :
+    {x : obj-Precategory C} →
+    left-unit-law-comp-hom-Precategory C (id-hom-Precategory C {x = x}) ＝
+    right-unit-law-comp-hom-Precategory C (id-hom-Precategory C {x = x})
+  coh-unit-laws-comp-hom-Precategory {x} =
+    eq-is-prop
+      ( is-set-hom-Precategory C x x
+        ( comp-hom-Precategory C (id-hom-Precategory C) (id-hom-Precategory C))
+        ( id-hom-Precategory C))
+```
+
+### Coherence between the associativity law and the unit laws of a precategory
+
+```agda
+module _
+  {l1 l2 : Level} (C : Precategory l1 l2)
+  where
+
+  coh-associative-left-unit-law-comp-hom-Precategory :
+    {x y z : obj-Precategory C}
+    {f : hom-Precategory C x y} {g : hom-Precategory C y z} →
+    ( associative-comp-hom-Precategory C (id-hom-Precategory C) g f) ∙
+    ( left-unit-law-comp-hom-Precategory C (comp-hom-Precategory C g f)) ＝
+    ( ap
+      ( comp-hom-Precategory' C f)
+      ( left-unit-law-comp-hom-Precategory C g))
+  coh-associative-left-unit-law-comp-hom-Precategory {x} {y} {z} {f} {g} =
+      eq-is-prop
+      ( is-set-hom-Precategory C x z
+        ( comp-hom-Precategory C
+          ( comp-hom-Precategory C (id-hom-Precategory C) g)
+          ( f))
+        ( comp-hom-Precategory C g f))
+
+  coh-associative-left-unit-law-comp-hom-Precategory'' :
+    {x y : obj-Precategory C} {f : hom-Precategory C x y} →
+    ( associative-comp-hom-Precategory C
+      ( id-hom-Precategory C)
+      ( id-hom-Precategory C)
+      ( f)) ∙
+    left-unit-law-comp-hom-Precategory C
+      ( comp-hom-Precategory C (id-hom-Precategory C) f) ∙
+    left-unit-law-comp-hom-Precategory C f ＝
+    ( ap
+      ( comp-hom-Precategory' C f)
+      ( left-unit-law-comp-hom-Precategory C (id-hom-Precategory C))) ∙
+    ( left-unit-law-comp-hom-Precategory C f)
+  coh-associative-left-unit-law-comp-hom-Precategory'' {x} {y} {f} =
+    eq-is-prop
+      ( is-set-hom-Precategory C x y
+        ( comp-hom-Precategory C
+          ( comp-hom-Precategory C
+            ( id-hom-Precategory C)
+            ( id-hom-Precategory C))
+          ( f))
+        ( f))
+```
+
 ## See also
 
 - [Categories](category-theory.categories.md) are univalent precategories.
diff --git a/src/foundation/dependent-identifications.lagda.md b/src/foundation/dependent-identifications.lagda.md
index 0db1b41f3c..fa4dda4374 100644
--- a/src/foundation/dependent-identifications.lagda.md
+++ b/src/foundation/dependent-identifications.lagda.md
@@ -46,8 +46,7 @@ module _
     (p' : dependent-identification B p x' y')
     (q' : dependent-identification B q x' y') →
     p' ＝ tr² B α x' ∙ q' → dependent-identification² B α p' q'
-  map-compute-dependent-identification² refl ._ refl refl =
-    refl
+  map-compute-dependent-identification² refl q p' q' = q'
 
   map-inv-compute-dependent-identification² :
     {x y : A} {p q : x ＝ y} (α : p ＝ q)
@@ -55,8 +54,7 @@ module _
     (p' : dependent-identification B p x' y')
     (q' : dependent-identification B q x' y') →
     dependent-identification² B α p' q' → p' ＝ tr² B α x' ∙ q'
-  map-inv-compute-dependent-identification² refl refl ._ refl =
-    refl
+  map-inv-compute-dependent-identification² refl q p' q' = q'
 
   is-section-map-inv-compute-dependent-identification² :
     {x y : A} {p q : x ＝ y} (α : p ＝ q)
@@ -65,8 +63,7 @@ module _
     (q' : dependent-identification B q x' y') →
     ( map-compute-dependent-identification² α p' q' ∘
       map-inv-compute-dependent-identification² α p' q') ~ id
-  is-section-map-inv-compute-dependent-identification² refl refl ._ refl =
-    refl
+  is-section-map-inv-compute-dependent-identification² refl q p' q' = refl
 
   is-retraction-map-inv-compute-dependent-identification² :
     {x y : A} {p q : x ＝ y} (α : p ＝ q)
@@ -75,8 +72,7 @@ module _
     (q' : dependent-identification B q x' y') →
     ( map-inv-compute-dependent-identification² α p' q' ∘
       map-compute-dependent-identification² α p' q') ~ id
-  is-retraction-map-inv-compute-dependent-identification² refl ._ refl refl =
-    refl
+  is-retraction-map-inv-compute-dependent-identification² refl q p' q' = refl
 
   is-equiv-map-compute-dependent-identification² :
     {x y : A} {p q : x ＝ y} (α : p ＝ q)
@@ -104,9 +100,9 @@ module _
 
 ### The groupoidal structure of dependent identifications
 
-We show that there is groupoidal structure on the dependent identifications. The
-statement of the groupoid laws use dependent identifications, due to the
-dependent nature of dependent identifications.
+We show that there is a dependent groupoidal structure on the dependent
+identifications. The statement of the groupoid laws use dependent
+identifications, due to the dependent nature of dependent identifications.
 
 #### Concatenation of dependent identifications
 
@@ -164,7 +160,7 @@ module _
     {x y : A} (p : x ＝ y) {x' : B x} {y' : B y} →
     dependent-identification B p x' y' →
     dependent-identification B (inv p) y' x'
-  inv-dependent-identification refl refl = refl
+  inv-dependent-identification refl = inv
 ```
 
 #### Associativity of concatenation of dependent identifications
@@ -276,7 +272,7 @@ module _
         ( inv p)
         ( inv-dependent-identification B p q))
       ( q)
-  inv-inv-dependent-identification refl refl = refl
+  inv-inv-dependent-identification refl = inv-inv
 ```
 
 ### The inverse distributes over concatenation of dependent identifications
diff --git a/src/type-theories/simple-type-theories.lagda.md b/src/type-theories/simple-type-theories.lagda.md
index 98461a1a5e..b8e45f3112 100644
--- a/src/type-theories/simple-type-theories.lagda.md
+++ b/src/type-theories/simple-type-theories.lagda.md
@@ -54,9 +54,9 @@ module simple where
     coinductive
     field
       element :
-        {X : T} (x : system.element A X) →
-        fibered-system.element B (f X) x
-      slice : (X : T) → section-system (fibered-system.slice B (f X)) f
+        {X : T} (x : system.element A X) → fibered-system.element B (f X) x
+      slice :
+        (X : T) → section-system (fibered-system.slice B (f X)) f
 
   ------------------------------------------------------------------------------
 ```