diff --git a/src/Categories/Category/Construction/Kleisli.agda b/src/Categories/Category/Construction/Kleisli.agda
index 6e8e68d27..47df61ad6 100644
--- a/src/Categories/Category/Construction/Kleisli.agda
+++ b/src/Categories/Category/Construction/Kleisli.agda
@@ -41,7 +41,7 @@ Kleisli {𝒞 = 𝒞} M = record
   assoc′ {A} {B} {C} {D} {f} {g} {h} = begin
     (μ.η D ∘ F₁ ((μ.η D ∘ F₁ h) ∘ g)) ∘ f           ≈⟨ pushʳ homomorphism ⟩∘⟨refl ⟩
     ((μ.η D ∘ F₁ (μ.η D ∘ F₁ h)) ∘ F₁ g) ∘ f        ≈⟨ pushˡ (∘-resp-≈ˡ (∘-resp-≈ʳ homomorphism)) ⟩
-    (μ.η D ∘ (F₁ (μ.η D) ∘ F₁ (F₁ h))) ∘ (F₁ g ∘ f) ≈⟨ pushˡ (glue′ M.assoc (μ.commute h)) ⟩
+    (μ.η D ∘ (F₁ (μ.η D) ∘ F₁ (F₁ h))) ∘ (F₁ g ∘ f) ≈⟨ pushˡ (sym-glue M.assoc (μ.commute h)) ⟩
     (μ.η D ∘ F₁ h) ∘ (μ.η C ∘ (F₁ g ∘ f))           ≈⟨ refl⟩∘⟨ sym-assoc ⟩
     (μ.η D ∘ F₁ h) ∘ ((μ.η C ∘ F₁ g) ∘ f)           ∎
 
diff --git a/src/Categories/Category/Construction/Total.agda b/src/Categories/Category/Construction/Total.agda
new file mode 100644
index 000000000..f6d261e66
--- /dev/null
+++ b/src/Categories/Category/Construction/Total.agda
@@ -0,0 +1,55 @@
+{-# OPTIONS --safe --without-K #-}
+
+open import Categories.Category.Core using (Category)
+open import Categories.Category.Displayed using (Displayed)
+
+module Categories.Category.Construction.Total {o ℓ e o′ ℓ′ e′} {B : Category o ℓ e} (C : Displayed B o′ ℓ′ e′) where
+
+open import Data.Product using (proj₁; proj₂; Σ-syntax; ∃-syntax; -,_)
+open import Level using (_⊔_)
+
+open import Categories.Functor.Core using (Functor)
+
+open Category B
+open Displayed C
+open Equiv′
+
+Total : Set (o ⊔ o′)
+Total = Σ[ Carrier ∈ Obj ] Obj[ Carrier ]
+
+record Total⇒ (X Y : Total) : Set (ℓ ⊔ ℓ′) where
+  constructor total⇒
+  field
+    {arr} : proj₁ X ⇒ proj₁ Y
+    preserves : proj₂ X ⇒[ arr ] proj₂ Y
+
+open Total⇒ public using (preserves)
+
+∫ : Category (o ⊔ o′) (ℓ ⊔ ℓ′) (e ⊔ e′)
+∫ = record
+  { Obj = Total
+  ; _⇒_ = Total⇒
+  ; _≈_ = λ f g → ∃[ p ] preserves f ≈[ p ] preserves g
+  ; id = total⇒ id′
+  ; _∘_ = λ f g → total⇒ (preserves f ∘′ preserves g)
+  ; assoc = -, assoc′
+  ; sym-assoc = -, sym-assoc′
+  ; identityˡ = -, identityˡ′
+  ; identityʳ = -, identityʳ′
+  ; identity² = -, identity²′
+  ; equiv = record
+    { refl = -, refl′
+    ; sym = λ p → -, sym′ (proj₂ p)
+    ; trans = λ p q → -, trans′ (proj₂ p) (proj₂ q)
+    }
+  ; ∘-resp-≈ = λ p q → -, ∘′-resp-[]≈ (proj₂ p) (proj₂ q)
+  }
+
+display : Functor ∫ B
+display = record
+  { F₀ = proj₁
+  ; F₁ = Total⇒.arr
+  ; identity = Equiv.refl
+  ; homomorphism = Equiv.refl
+  ; F-resp-≈ = proj₁
+  }
diff --git a/src/Categories/Category/Displayed.agda b/src/Categories/Category/Displayed.agda
new file mode 100644
index 000000000..882b90cd8
--- /dev/null
+++ b/src/Categories/Category/Displayed.agda
@@ -0,0 +1,118 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category
+
+module Categories.Category.Displayed where
+
+open import Data.Product
+open import Level
+
+open import Categories.Functor.Core
+open import Relation.Binary.Displayed
+import Relation.Binary.Displayed.Reasoning.Setoid as DisplayedSetoidR
+
+-- A displayed category captures the idea of placing extra structure
+-- over a base category. For example, the category of monoids can be
+-- considered as the category of setoids with extra structure on the
+-- objects and extra conditions on the morphisms.
+record Displayed {o ℓ e} (B : Category o ℓ e) o′ ℓ′ e′ : Set (o ⊔ ℓ ⊔ e ⊔ suc (o′ ⊔ ℓ′ ⊔ e′)) where
+  open Category B
+  open Equiv
+
+  infix 4 _⇒[_]_ _≈[_]_
+  infixr 9 _∘′_
+
+  field
+    Obj[_] : Obj → Set o′
+    _⇒[_]_ : ∀ {X Y} → Obj[ X ] → X ⇒ Y → Obj[ Y ] → Set ℓ′
+    _≈[_]_ : ∀ {A B X Y} {f g : A ⇒ B} → X ⇒[ f ] Y → f ≈ g → X ⇒[ g ] Y → Set e′
+
+    id′ : ∀ {A} {X : Obj[ A ]} → X ⇒[ id ] X
+    _∘′_ : ∀ {A B C X Y Z} {f : B ⇒ C} {g : A ⇒ B}
+         → Y ⇒[ f ] Z → X ⇒[ g ] Y → X ⇒[ f ∘ g ] Z
+
+    identityʳ′ : ∀ {A B X Y} {f : A ⇒ B} → {f′ : X ⇒[ f ] Y} → f′ ∘′ id′ ≈[ identityʳ ] f′
+    identityˡ′ : ∀ {A B X Y} {f : A ⇒ B} → {f′ : X ⇒[ f ] Y} → id′ ∘′ f′ ≈[ identityˡ ] f′
+    identity²′ : ∀ {A} {X : Obj[ A ]} → id′ {X = X} ∘′ id′ ≈[ identity² ] id′
+    assoc′ : ∀ {A B C D W X Y Z} {f : C ⇒ D} {g : B ⇒ C} {h : A ⇒ B}
+           → {f′ : Y ⇒[ f ] Z} → {g′ : X ⇒[ g ] Y} → {h′ : W ⇒[ h ] X}
+           → (f′ ∘′ g′) ∘′ h′ ≈[ assoc ] f′ ∘′ (g′ ∘′ h′)
+    sym-assoc′ : ∀ {A B C D W X Y Z} {f : C ⇒ D} {g : B ⇒ C} {h : A ⇒ B}
+           → {f′ : Y ⇒[ f ] Z} → {g′ : X ⇒[ g ] Y} → {h′ : W ⇒[ h ] X}
+           → f′ ∘′ (g′ ∘′ h′) ≈[ sym-assoc ] (f′ ∘′ g′) ∘′ h′
+
+
+    equiv′ : ∀ {A B X Y} → IsDisplayedEquivalence equiv (_≈[_]_ {A} {B} {X} {Y})
+
+    ∘′-resp-≈[] : ∀ {A B C X Y Z} {f h : B ⇒ C} {g i : A ⇒ B}
+                    {f′ : Y ⇒[ f ] Z} {h′ : Y ⇒[ h ] Z} {g′ : X ⇒[ g ] Y} {i′ : X ⇒[ i ] Y}
+                    {p : f ≈ h} {q : g ≈ i}
+                → f′ ≈[ p ] h′ → g′ ≈[ q ] i′ → f′ ∘′ g′ ≈[ ∘-resp-≈ p q ] h′ ∘′ i′
+
+  module Equiv′ {A B X Y} = IsDisplayedEquivalence (equiv′ {A} {B} {X} {Y})
+
+  open Equiv′
+
+  ∘′-resp-≈[]ˡ : ∀ {A B C X Y Z} {f h : B ⇒ C} {g : A ⇒ B} {f′ : Y ⇒[ f ] Z} {h′ : Y ⇒[ h ] Z} {g′ : X ⇒[ g ] Y}
+                 → {p : f ≈ h} → f′ ≈[ p ] h′ → f′ ∘′ g′ ≈[ ∘-resp-≈ˡ p ] h′ ∘′ g′
+  ∘′-resp-≈[]ˡ pf = ∘′-resp-≈[] pf refl′
+
+  ∘′-resp-≈[]ʳ : ∀ {A B C X Y Z} {f : B ⇒ C} {g i : A ⇒ B} {f′ : Y ⇒[ f ] Z} {g′ : X ⇒[ g ] Y} {i′ : X ⇒[ i ] Y}
+                 → {p : g ≈ i} → g′ ≈[ p ] i′ → f′ ∘′ g′ ≈[ ∘-resp-≈ʳ p ] f′ ∘′ i′
+  ∘′-resp-≈[]ʳ pf = ∘′-resp-≈[] refl′ pf
+
+  hom-setoid′ : ∀ {A B} {X : Obj[ A ]} {Y : Obj[ B ]} → DisplayedSetoid hom-setoid _ _
+  hom-setoid′ {X = X} {Y = Y} = record
+    { Carrier′ = X ⇒[_] Y
+    ; _≈[_]_ = _≈[_]_
+    ; isDisplayedEquivalence = equiv′
+    }
+
+  module HomReasoning′ {A B : Obj} {X : Obj[ A ]} {Y : Obj[ B ]} where
+    open DisplayedSetoidR (hom-setoid′ {X = X} {Y = Y}) public
+    open HomReasoning
+
+    infixr 4 _⟩∘′⟨_ refl′⟩∘′⟨_
+    infixl 5 _⟩∘′⟨refl′
+    _⟩∘′⟨_ : ∀ {M} {f h : M ⇒ B} {g i : A ⇒ M} {f≈h : f ≈ h} {g≈i : g ≈ i}
+               {M′ : Obj[ M ]} {f′ : M′ ⇒[ f ] Y} {h′ : M′ ⇒[ h ] Y} {g′ : X ⇒[ g ] M′} {i′ : X ⇒[ i ] M′}
+             → f′ ≈[ f≈h ] h′ → g′ ≈[ g≈i ] i′ → f′ ∘′ g′ ≈[ f≈h ⟩∘⟨ g≈i ] h′ ∘′ i′
+    _⟩∘′⟨_ = ∘′-resp-≈[]
+
+    refl′⟩∘′⟨_ : ∀ {M} {f : M ⇒ B} {g i : A ⇒ M} {g≈i : g ≈ i}
+                  {M′ : Obj[ M ]} {f′ : M′ ⇒[ f ] Y} {g′ : X ⇒[ g ] M′} {i′ : X ⇒[ i ] M′}
+                → g′ ≈[ g≈i ] i′ → f′ ∘′ g′ ≈[ refl⟩∘⟨ g≈i ] f′ ∘′ i′
+    refl′⟩∘′⟨_ = ∘′-resp-≈[]ʳ
+
+    _⟩∘′⟨refl′ : ∀ {M} {f h : M ⇒ B} {g : A ⇒ M} {f≈h : f ≈ h}
+                   {M′ : Obj[ M ]} {f′ : M′ ⇒[ f ] Y} {h′ : M′ ⇒[ h ] Y} {g′ : X ⇒[ g ] M′}
+                 → f′ ≈[ f≈h ] h′ → f′ ∘′ g′ ≈[ f≈h ⟩∘⟨refl ] h′ ∘′ g′
+    _⟩∘′⟨refl′ = ∘′-resp-≈[]ˡ
+
+  op′ : Displayed op o′ ℓ′ e′
+  op′ = record
+    { Obj[_] = Obj[_]
+    ; _⇒[_]_ = λ X f Y → Y ⇒[ f ] X
+    ; _≈[_]_ = _≈[_]_
+    ; id′ = id′
+    ; _∘′_ = λ f′ g′ → g′ ∘′ f′
+    ; identityʳ′ = identityˡ′
+    ; identityˡ′ = identityʳ′
+    ; identity²′ = identity²′
+    ; assoc′ = sym-assoc′
+    ; sym-assoc′ = assoc′
+    ; equiv′ = equiv′
+    ; ∘′-resp-≈[] = λ p q → ∘′-resp-≈[] q p
+    }
+
+module Definitions′ {o ℓ e} {B : Category o ℓ e} {o′ ℓ′ e′} (C : Displayed B o′ ℓ′ e′) where
+  open Category B
+  open Displayed C
+  open Definitions B
+
+  CommutativeSquare′ : ∀ {A B C D : Obj} {A′ : Obj[ A ]} {B′ : Obj[ B ]} {C′ : Obj[ C ]} {D′ : Obj[ D ]}
+                         {f : A ⇒ B} {g : A ⇒ C} {h : B ⇒ D} {i : C ⇒ D}
+                         (f′ : A′ ⇒[ f ] B′) (g′ : A′ ⇒[ g ] C′) (h′ : B′ ⇒[ h ] D′) (i′ : C′ ⇒[ i ] D′)
+                         (sq : CommutativeSquare f g h i)
+                       → Set _
+  CommutativeSquare′ f′ g′ h′ i′ sq = h′ ∘′ f′ ≈[ sq ] i′ ∘′ g′
diff --git a/src/Categories/Category/Displayed/Instance/DisplayedCats.agda b/src/Categories/Category/Displayed/Instance/DisplayedCats.agda
new file mode 100644
index 000000000..5349c4212
--- /dev/null
+++ b/src/Categories/Category/Displayed/Instance/DisplayedCats.agda
@@ -0,0 +1,27 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Categories.Category.Displayed.Instance.DisplayedCats where
+
+open import Level
+
+open import Categories.Category
+open import Categories.Category.Displayed
+open import Categories.Category.Instance.Cats
+open import Categories.Functor.Displayed
+open import Categories.NaturalTransformation.NaturalIsomorphism.Displayed
+
+DisplayedCats : ∀ o ℓ e o′ ℓ′ e′ → Displayed (Cats o ℓ e) (o ⊔ ℓ ⊔ e ⊔ suc (o′ ⊔ ℓ′ ⊔ e′)) (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) (o ⊔ ℓ ⊔ o′ ⊔ ℓ′ ⊔ e′)
+DisplayedCats o ℓ e o′ ℓ′ e′ = record
+  { Obj[_] = λ B → Displayed B o′ ℓ′ e′
+  ; _⇒[_]_ = λ C F D → DisplayedFunctor C D F
+  ; _≈[_]_ = λ F′ F≃G G′ → DisplayedNaturalIsomorphism F′ G′ F≃G
+  ; id′ = id′
+  ; _∘′_ = _∘F′_
+  ; identityˡ′ = unitorˡ′
+  ; identityʳ′ = unitorʳ′
+  ; identity²′ = unitor²′
+  ; assoc′ = λ {_ _ _ _ _ _ _ _ _ _ _ F′ G′ H′} → associator′ H′ G′ F′
+  ; sym-assoc′ = λ {_ _ _ _ _ _ _ _ _ _ _ F′ G′ H′} → sym-associator′ H′ G′ F′
+  ; equiv′ = isDisplayedEquivalence
+  ; ∘′-resp-≈[] = _ⓘₕ′_
+  }
diff --git a/src/Categories/Category/Instance/Cats.agda b/src/Categories/Category/Instance/Cats.agda
index 77b2ab8bf..116d2d9e9 100644
--- a/src/Categories/Category/Instance/Cats.agda
+++ b/src/Categories/Category/Instance/Cats.agda
@@ -9,7 +9,7 @@ open import Level
 open import Categories.Category using (Category)
 open import Categories.Functor using (Functor; id; _∘F_)
 open import Categories.NaturalTransformation.NaturalIsomorphism
-  using (NaturalIsomorphism; associator; unitorˡ; unitorʳ; unitor²; isEquivalence; _ⓘₕ_; sym)
+  using (NaturalIsomorphism; associator; sym-associator; unitorˡ; unitorʳ; unitor²; isEquivalence; _ⓘₕ_; sym)
 private
   variable
     o ℓ e : Level
@@ -24,7 +24,7 @@ Cats o ℓ e = record
   ; id        = id
   ; _∘_       = _∘F_
   ; assoc     = λ {_ _ _ _ F G H} → associator F G H
-  ; sym-assoc = λ {_ _ _ _ F G H} → sym (associator F G H)
+  ; sym-assoc = λ {_ _ _ _ F G H} → sym-associator F G H
   ; identityˡ = unitorˡ
   ; identityʳ = unitorʳ
   ; identity² = unitor²
diff --git a/src/Categories/Functor/Displayed.agda b/src/Categories/Functor/Displayed.agda
new file mode 100644
index 000000000..aeb36b4ad
--- /dev/null
+++ b/src/Categories/Functor/Displayed.agda
@@ -0,0 +1,77 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Categories.Functor.Displayed where
+
+open import Function.Base using () renaming (id to id→; _∘_ to _∙_)
+open import Level
+
+open import Categories.Category
+open import Categories.Category.Displayed
+open import Categories.Functor
+
+private
+  variable
+    o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ o‴ ℓ‴ e‴  : Level
+    B₁ B₂ B₃ : Category o ℓ e
+
+record DisplayedFunctor {B₁ : Category o ℓ e} {B₂ : Category o′ ℓ′ e′} (C : Displayed B₁ o″ ℓ″ e″) (D : Displayed B₂ o‴ ℓ‴ e‴) (F : Functor B₁ B₂) : Set (o ⊔ ℓ ⊔ e ⊔ o″ ⊔ ℓ″ ⊔ e″ ⊔ o‴ ⊔ ℓ‴ ⊔ e‴) where
+  private
+    module C = Displayed C
+    module D = Displayed D
+    module F = Functor F
+  field
+    F₀′ : ∀ {X} → C.Obj[ X ] → D.Obj[ F.₀ X ]
+    F₁′ : ∀ {X Y} {f : B₁ [ X , Y ]} {X′ Y′} → X′ C.⇒[ f ] Y′ → F₀′ X′ D.⇒[ F.₁ f ] F₀′ Y′
+    identity′ : ∀ {X} {X′ : C.Obj[ X ]} → F₁′ (C.id′ {X = X′}) D.≈[ F.identity ] D.id′
+    homomorphism′ : ∀ {X Y Z} {X′ : C.Obj[ X ]} {Y′ : C.Obj[ Y ]} {Z′ : C.Obj[ Z ]}
+                      {f : B₁ [ X , Y ]} {g : B₁ [ Y , Z ]} {f′ : X′ C.⇒[ f ] Y′} {g′ : Y′ C.⇒[ g ] Z′}
+                    → F₁′ (g′ C.∘′ f′) D.≈[ F.homomorphism ] F₁′ g′ D.∘′ F₁′ f′
+    F′-resp-≈[] : ∀ {X Y} {X′ : C.Obj[ X ]} {Y′ : C.Obj[ Y ]}
+                    {f g : B₁ [ X , Y ]} {f′ : X′ C.⇒[ f ] Y′} {g′ : X′ C.⇒[ g ] Y′}
+                  → {p : B₁ [ f ≈ g ]} → f′ C.≈[ p ] g′
+                  → F₁′ f′ D.≈[ F.F-resp-≈ p ] F₁′ g′
+
+  ₀′ = F₀′
+  ₁′ = F₁′
+
+  op′ : DisplayedFunctor C.op′ D.op′ F.op
+  op′ = record
+    { F₀′ = F₀′
+    ; F₁′ = F₁′
+    ; identity′ = identity′
+    ; homomorphism′ = homomorphism′
+    ; F′-resp-≈[] = F′-resp-≈[]
+    }
+
+id′ : ∀ {B : Category o ℓ e} {C : Displayed B o′ ℓ′ e′} → DisplayedFunctor C C id
+id′ {C = C} = record
+  { F₀′ = id→
+  ; F₁′ = id→
+  ; identity′ = Displayed.Equiv′.refl′ C
+  ; homomorphism′ = Displayed.Equiv′.refl′ C
+  ; F′-resp-≈[] = id→
+  }
+
+_∘F′_ : ∀ {C : Displayed B₁ o ℓ e} {D : Displayed B₂ o′ ℓ′ e′} {E : Displayed B₃ o″ ℓ″ e″}
+          {F : Functor B₂ B₃} {G : Functor B₁ B₂}
+        → DisplayedFunctor D E F → DisplayedFunctor C D G → DisplayedFunctor C E (F ∘F G)
+_∘F′_  {C = C} {D = D} {E = E} F′ G′ = record
+   { F₀′ = F′.₀′ ∙ G′.₀′
+   ; F₁′ = F′.₁′ ∙ G′.₁′
+   ; identity′ = begin′
+     F′.₁′ (G′.₁′ C.id′) ≈[]⟨ F′.F′-resp-≈[] G′.identity′ ⟩
+     F′.₁′ D.id′         ≈[]⟨ F′.identity′ ⟩
+     E.id′               ∎′
+   ; homomorphism′ = λ {_} {_} {_} {_} {_} {_} {_} {_} {f′} {g′} → begin′
+     F′.₁′ (G′.₁′ (g′ C.∘′ f′))               ≈[]⟨ F′.F′-resp-≈[] G′.homomorphism′ ⟩
+     F′.₁′ (G′.₁′ g′ D.∘′ G′.₁′ f′)           ≈[]⟨ F′.homomorphism′ ⟩
+     (F′.₁′ (G′.₁′ g′) E.∘′ F′.₁′ (G′.₁′ f′)) ∎′
+   ; F′-resp-≈[] = F′.F′-resp-≈[] ∙ G′.F′-resp-≈[]
+   }
+   where
+     module C = Displayed C
+     module D = Displayed D
+     module E = Displayed E
+     open E.HomReasoning′
+     module F′ = DisplayedFunctor F′
+     module G′ = DisplayedFunctor G′
diff --git a/src/Categories/Functor/Displayed/Properties.agda b/src/Categories/Functor/Displayed/Properties.agda
new file mode 100644
index 000000000..d39fb52d9
--- /dev/null
+++ b/src/Categories/Functor/Displayed/Properties.agda
@@ -0,0 +1,67 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Categories.Functor.Displayed.Properties where
+
+open import Categories.Category
+open import Categories.Category.Displayed
+open import Categories.Functor
+open import Categories.Functor.Displayed
+open import Categories.Functor.Properties
+open import Categories.Morphism
+open import Categories.Morphism.Displayed
+
+module _
+  {o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ o‴ ℓ‴ e‴}
+  {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {F : Functor C D}
+  {C′ : Displayed C o″ ℓ″ e″} {D′ : Displayed D o‴ ℓ‴ e‴} (F′ : DisplayedFunctor C′ D′ F)
+  where
+
+  private
+    module C = Category C
+--    module F = Functor F
+    module C′ = Displayed C′
+    module D′ = Displayed D′
+    module F′ = DisplayedFunctor F′
+
+  open Definitions
+  open Definitions′
+
+  [_]-resp-∘′ : ∀ {X Y Z} {f : Y C.⇒ Z} {g : X C.⇒ Y} {h : X C.⇒ Z} {f∘g≈h : f C.∘ g C.≈ h}
+                  {X′  : C′.Obj[ X ]} {Y′ : C′.Obj[ Y ]} {Z′ : C′.Obj[ Z ]}
+                  {f′ : Y′ C′.⇒[ f ] Z′} {g′ : X′ C′.⇒[ g ] Y′} {h′ : X′ C′.⇒[ h ] Z′}
+                → f′ C′.∘′ g′ C′.≈[ f∘g≈h ] h′
+                → F′.₁′ f′ D′.∘′ F′.₁′ g′ D′.≈[ [ F ]-resp-∘ f∘g≈h ] F′.₁′ h′
+  [_]-resp-∘′ {f′ = f′} {g′ = g′} {h′ = h′} eq = begin′
+    F′.₁′ f′ D′.∘′ F′.₁′ g′ ≈˘[]⟨ F′.homomorphism′ ⟩
+    F′.₁′ (f′ C′.∘′ g′)     ≈[]⟨ F′.F′-resp-≈[] eq ⟩
+    F′.₁′ h′                ∎′
+    where open D′.HomReasoning′
+
+  [_]-resp-square′ : ∀ {W X Y Z} {f : W C.⇒ X} {g : W C.⇒ Y} {h : X C.⇒ Z} {i : Y C.⇒ Z} {sq : CommutativeSquare C f g h i}
+                       {W′ : C′.Obj[ W ]} {X′ : C′.Obj[ X ]} {Y′ : C′.Obj[ Y ]} {Z′ : C′.Obj[ Z ]}
+                       {f′ : W′ C′.⇒[ f ] X′} {g′ : W′ C′.⇒[ g ] Y′} {h′ : X′ C′.⇒[ h ] Z′} {i′ : Y′ C′.⇒[ i ] Z′}
+                    → CommutativeSquare′ C′ f′ g′ h′ i′ sq
+                    → CommutativeSquare′ D′ (F′.₁′ f′) (F′.₁′ g′) (F′.₁′ h′) (F′.₁′ i′) ([ F ]-resp-square sq)
+  [_]-resp-square′ {f′ = f′} {g′ = g′} {h′ = h′} {i′ = i′} sq′ = begin′
+    F′.₁′ h′ D′.∘′ F′.₁′ f′ ≈˘[]⟨ F′.homomorphism′ ⟩
+    F′.₁′ (h′ C′.∘′ f′)     ≈[]⟨ F′.F′-resp-≈[] sq′ ⟩
+    F′.₁′ (i′ C′.∘′ g′)     ≈[]⟨ F′.homomorphism′ ⟩
+    F′.₁′ i′ D′.∘′ F′.₁′ g′ ∎′
+    where open D′.HomReasoning′
+
+  [_]-resp-DisplayedIso : ∀ {X Y} {f : X C.⇒ Y} {g : Y C.⇒ X} {iso : Iso C f g}
+                            {X′ : C′.Obj[ X ]} {Y′ : C′.Obj[ Y ]} {f′ : X′ C′.⇒[ f ] Y′} {g′ : Y′ C′.⇒[ g ] X′}
+                          → DisplayedIso C′ f′ g′ iso → DisplayedIso D′ (F′.₁′ f′) (F′.₁′ g′) ([ F ]-resp-Iso iso)
+  [_]-resp-DisplayedIso {f′ = f′} {g′ = g′} diso = record
+    { isoˡ′ = begin′
+      F′.₁′ g′ D′.∘′ F′.₁′ f′ ≈[]⟨ [ isoˡ′ ]-resp-∘′ ⟩
+      F′.₁′ C′.id′            ≈[]⟨ F′.identity′ ⟩
+      D′.id′                  ∎′
+    ; isoʳ′ = begin′
+      F′.₁′ f′ D′.∘′ F′.₁′ g′ ≈[]⟨ [ isoʳ′ ]-resp-∘′ ⟩
+      F′.₁′ C′.id′            ≈[]⟨ F′.identity′ ⟩
+      D′.id′                  ∎′
+    }
+    where
+      open DisplayedIso diso
+      open D′.HomReasoning′
diff --git a/src/Categories/Morphism/Displayed.agda b/src/Categories/Morphism/Displayed.agda
new file mode 100644
index 000000000..2ac074e67
--- /dev/null
+++ b/src/Categories/Morphism/Displayed.agda
@@ -0,0 +1,23 @@
+{-# OPTIONS --safe --without-K #-}
+
+open import Categories.Category
+open import Categories.Category.Displayed
+
+module Categories.Morphism.Displayed {o ℓ e o′ ℓ′ e′} {B : Category o ℓ e} (C : Displayed B o′ ℓ′ e′) where
+
+open import Categories.Morphism B
+
+open Category B
+open Displayed C
+
+private
+  variable
+    X Y : Obj
+    X′ : Obj[ X ]
+    Y′ : Obj[ Y ]
+
+record DisplayedIso {from : X ⇒ Y} {to : Y ⇒ X} (from′ : X′ ⇒[ from ] Y′) (to′ : Y′ ⇒[ to ] X′) (iso : Iso from to) : Set e′ where
+  open Iso iso
+  field
+    isoˡ′ : to′ ∘′ from′ ≈[ isoˡ ] id′
+    isoʳ′ : from′ ∘′ to′ ≈[ isoʳ ] id′
diff --git a/src/Categories/Morphism/Displayed/Properties.agda b/src/Categories/Morphism/Displayed/Properties.agda
new file mode 100644
index 000000000..8b7852924
--- /dev/null
+++ b/src/Categories/Morphism/Displayed/Properties.agda
@@ -0,0 +1,54 @@
+{-# OPTIONS --safe --without-K #-}
+
+open import Categories.Category.Core
+open import Categories.Category.Displayed
+
+module Categories.Morphism.Displayed.Properties {o ℓ e o′ ℓ′ e′} {B : Category o ℓ e} (C : Displayed B o′ ℓ′ e′) where
+
+open import Categories.Morphism B
+open import Categories.Morphism.Displayed C
+open import Categories.Morphism.Displayed.Reasoning C
+open import Categories.Morphism.Properties B
+
+open Category B
+open Displayed C
+open HomReasoning′
+
+private
+  variable
+    X Y : Obj
+    X′ Y′ Z′ : Obj[ X ]
+    f g h i : X ⇒ Y
+    h′ i′ : X′ ⇒[ f ] Y′
+
+module _ {f′ : X′ ⇒[ f ] Y′} {g′ : Y′ ⇒[ g ] X′} {iso : Iso f g} (diso : DisplayedIso f′ g′ iso) where
+
+  open DisplayedIso diso
+
+  DisplayedIso-resp-≈[] : {f≈h : f ≈ h} {g≈i : g ≈ i} → f′ ≈[ f≈h ] h′ → g′ ≈[ g≈i ] i′ → DisplayedIso h′ i′ (Iso-resp-≈ iso f≈h g≈i)
+  DisplayedIso-resp-≈[] {h′ = h′} {i′ = i′} f′≈h′ g′≈i′ = record
+    { isoˡ′ = begin′
+      i′ ∘′ h′ ≈˘[]⟨ g′≈i′ ⟩∘′⟨ f′≈h′ ⟩
+      g′ ∘′ f′ ≈[]⟨ isoˡ′ ⟩
+      id′      ∎′
+    ; isoʳ′ = begin′
+      h′ ∘′ i′ ≈˘[]⟨ f′≈h′ ⟩∘′⟨ g′≈i′ ⟩
+      f′ ∘′ g′ ≈[]⟨ isoʳ′ ⟩
+      id′      ∎′
+    }
+
+DisplayedIso-∘′ : {f′ : X′ ⇒[ f ] Y′} {g′ : Y′ ⇒[ g ] X′} {h′ : Y′ ⇒[ h ] Z′} {i′ : Z′ ⇒[ i ] Y′}
+                → {f≅g : Iso f g} {h≅i : Iso h i}
+                → DisplayedIso f′ g′ f≅g → DisplayedIso h′ i′ h≅i
+                → DisplayedIso (h′ ∘′ f′) (g′ ∘′ i′) (Iso-∘ f≅g h≅i)
+DisplayedIso-∘′ {f′ = f′} {g′ = g′} {h′ = h′} {i′ = i′} f′≅g′ h′≅i′ = record
+  { isoˡ′ = begin′
+    (g′ ∘′ i′) ∘′ (h′ ∘′ f′) ≈[]⟨ cancelInner′ (isoˡ′ h′≅i′) ⟩
+    g′ ∘′ f′                 ≈[]⟨ isoˡ′ f′≅g′ ⟩
+    id′                      ∎′
+  ; isoʳ′ = begin′
+    (h′ ∘′ f′) ∘′ (g′ ∘′ i′) ≈[]⟨ cancelInner′ (isoʳ′ f′≅g′) ⟩
+    h′ ∘′ i′                 ≈[]⟨ isoʳ′ h′≅i′ ⟩
+    id′                      ∎′
+  }
+  where open DisplayedIso
diff --git a/src/Categories/Morphism/Displayed/Reasoning.agda b/src/Categories/Morphism/Displayed/Reasoning.agda
new file mode 100644
index 000000000..ed8a3da7d
--- /dev/null
+++ b/src/Categories/Morphism/Displayed/Reasoning.agda
@@ -0,0 +1,107 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- Utilities for reasoning about displayed morphisms
+
+open import Categories.Category
+open import Categories.Category.Displayed
+
+module Categories.Morphism.Displayed.Reasoning {o ℓ e o′ ℓ′ e′} {B : Category o ℓ e} (C : Displayed B o′ ℓ′ e′) where
+
+open import Categories.Morphism.Reasoning.Core B
+
+open Category B
+open Definitions B
+open Displayed C
+open Equiv′
+open HomReasoning′
+open Definitions′ C
+
+private
+  variable
+    X Y : Obj
+    f g h i j k l a b c : X ⇒ Y
+    X′ Y′ : Obj[ X ]
+    f′ g′ h′ i′ j′ k′ l′ a′ b′ c′ : X′ ⇒[ f ] Y′
+
+module Identity′ where
+  id′-comm : ∀ {A B X Y} {f : A ⇒ B} {f′ : X ⇒[ f ] Y} → f′ ∘′ id′ ≈[ id-comm ] id′ ∘′ f′
+  id′-comm = trans′ identityʳ′ (sym′ identityˡ′)
+
+  id′-comm-sym : ∀ {A B X Y} {f : A ⇒ B} {f′ : X ⇒[ f ] Y} → id′ ∘′ f′ ≈[ id-comm-sym ] f′ ∘′ id′
+  id′-comm-sym = trans′ identityˡ′ (sym′ identityʳ′)
+
+open Identity′ public
+
+module Pulls′ {ab≈c : a ∘ b ≈ c} (a′b′≈[]c′ : a′ ∘′ b′ ≈[ ab≈c ] c′) where
+
+  pullʳ′ : (f′ ∘′ a′) ∘′ b′ ≈[ pullʳ ab≈c ] f′ ∘′ c′
+  pullʳ′ {f′ = f′} = begin′
+    (f′ ∘′ a′) ∘′ b′ ≈[]⟨ assoc′ ⟩
+    f′ ∘′ (a′ ∘′ b′) ≈[]⟨ refl′⟩∘′⟨ a′b′≈[]c′ ⟩
+    f′ ∘′ c′         ∎′
+
+  pullˡ′ : a′ ∘′ (b′ ∘′ f′) ≈[ pullˡ ab≈c ] c′ ∘′ f′
+  pullˡ′ {f′ = f′} = begin′
+    a′ ∘′ (b′ ∘′ f′) ≈[]⟨ sym-assoc′ ⟩
+    (a′ ∘′ b′) ∘′ f′ ≈[]⟨ a′b′≈[]c′ ⟩∘′⟨refl′ ⟩
+    c′ ∘′ f′         ∎′
+
+open Pulls′ public
+
+module Extends′ {s : CommutativeSquare f g h i} (s′ : CommutativeSquare′ f′ g′ h′ i′ s) where
+  extendˡ′ : CommutativeSquare′ f′ g′ (a′ ∘′ h′) (a′ ∘′ i′) (extendˡ s)
+  extendˡ′ {a′ = a′} = begin′
+    (a′ ∘′ h′) ∘′ f′ ≈[]⟨ pullʳ′ s′ ⟩
+    a′ ∘′ (i′ ∘′ g′) ≈[]⟨ sym-assoc′ ⟩
+    (a′ ∘′ i′) ∘′ g′ ∎′
+
+  extendʳ′ : CommutativeSquare′ (f′ ∘′ a′) (g′ ∘′ a′) h′ i′ (extendʳ s)
+  extendʳ′ {a′ = a′} = begin′
+    h′ ∘′ (f′ ∘′ a′) ≈[]⟨ pullˡ′ s′ ⟩
+    (i′ ∘′ g′) ∘′ a′ ≈[]⟨ assoc′ ⟩
+    i′ ∘′ (g′ ∘′ a′) ∎′
+
+  extend²′ : CommutativeSquare′ (f′ ∘′ b′) (g′ ∘′ b′) (a′ ∘′ h′) (a′ ∘′ i′) (extend² s)
+  extend²′ {b′ = b′} {a′ = a′} = begin′
+    (a′ ∘′ h′) ∘′ (f′ ∘′ b′) ≈[]⟨ pullʳ′ extendʳ′ ⟩
+    a′ ∘′ (i′ ∘′ (g′ ∘′ b′)) ≈[]⟨ sym-assoc′ ⟩
+    (a′ ∘′ i′) ∘′ (g′ ∘′ b′) ∎′
+
+open Extends′ public
+
+glue′ : ∀ {sq₁ : CommutativeSquare f g h i} {sq₂ : CommutativeSquare j k l f}
+        → CommutativeSquare′ f′ g′ h′ i′ sq₁
+        → CommutativeSquare′ j′ k′ l′ f′ sq₂
+        → CommutativeSquare′ j′ (g′ ∘′ k′) (h′ ∘′ l′) i′ (glue sq₁ sq₂)
+glue′ {f′ = f′} {g′ = g′} {h′ = h′} {i′ = i′} {j′ = j′} {k′ = k′} {l′ = l′} sq₁′ sq₂′ = begin′
+  (h′ ∘′ l′) ∘′ j′ ≈[]⟨ pullʳ′ sq₂′ ⟩
+  h′ ∘′ (f′ ∘′ k′) ≈[]⟨ extendʳ′ sq₁′ ⟩
+  i′ ∘′ (g′ ∘′ k′) ∎′
+
+sym-glue′ : ∀ {sq₁ : CommutativeSquare f g h i} {sq₂ : CommutativeSquare j k g l}
+            → CommutativeSquare′ f′ g′ h′ i′ sq₁
+            → CommutativeSquare′ j′ k′ g′ l′ sq₂
+            → CommutativeSquare′ (f′ ∘′ j′) k′ h′ (i′ ∘′ l′) (sym-glue sq₁ sq₂)
+sym-glue′ {f′ = f′} {g′ = g′} {h′ = h′} {i′ = i′} {j′ = j′} {k′ = k′} {l′ = l′} sq₁′ sq₂′ = begin′
+  h′ ∘′ (f′ ∘′ j′) ≈[]⟨ pullˡ′ sq₁′ ⟩
+  (i′ ∘′ g′) ∘′ j′ ≈[]⟨ extendˡ′ sq₂′ ⟩
+  (i′ ∘′ l′) ∘′ k′ ∎′
+
+module Cancellers′ {inv : h ∘ i ≈ id} (inv′ : h′ ∘′ i′ ≈[ inv ] id′) where
+
+  cancelʳ′ : (f′ ∘′ h′) ∘′ i′ ≈[ cancelʳ inv ] f′
+  cancelʳ′ {f′ = f′} = begin′
+    (f′ ∘′ h′) ∘′ i′ ≈[]⟨ pullʳ′ inv′ ⟩
+    f′ ∘′ id′        ≈[]⟨ identityʳ′ ⟩
+    f′               ∎′
+
+  cancelˡ′ : h′ ∘′ (i′ ∘′ f′) ≈[ cancelˡ inv ] f′
+  cancelˡ′ {f′ = f′} = begin′
+    h′ ∘′ (i′ ∘′ f′) ≈[]⟨ pullˡ′ inv′ ⟩
+    id′ ∘′ f′        ≈[]⟨ identityˡ′ ⟩
+    f′               ∎′
+
+  cancelInner′ : (f′ ∘′ h′) ∘′ (i′ ∘′ g′) ≈[ cancelInner inv ] f′ ∘′ g′
+  cancelInner′ = pullˡ′ cancelʳ′
+
+open Cancellers′ public
diff --git a/src/Categories/Morphism/Reasoning/Core.agda b/src/Categories/Morphism/Reasoning/Core.agda
index e30e1cd5a..65adfe03a 100644
--- a/src/Categories/Morphism/Reasoning/Core.agda
+++ b/src/Categories/Morphism/Reasoning/Core.agda
@@ -171,11 +171,11 @@ glue {c′ = c′} {a′ = a′} {a = a} {c″ = c″} {c = c} {b′ = b′} {b
   a ∘ (c′ ∘ b′)  ≈⟨ extendʳ sq-a ⟩
   c″ ∘ (a′ ∘ b′) ∎
 
--- A "rotated" version of glue′. Equivalent to 'Equiv.sym (glue (Equiv.sym sq-a) (Equiv.sym sq-b))'
-glue′ : CommutativeSquare a′ c′ c″ a →
-        CommutativeSquare b′ c c′ b →
-        CommutativeSquare (a′ ∘ b′) c c″ (a ∘ b)
-glue′ {a′ = a′} {c′ = c′} {c″ = c″} {a = a} {b′ = b′} {c = c} {b = b} sq-a sq-b = begin
+-- A "rotated" version of glue. Equivalent to 'Equiv.sym (glue (Equiv.sym sq-a) (Equiv.sym sq-b))'
+sym-glue : CommutativeSquare a′ c′ c″ a →
+           CommutativeSquare b′ c c′ b →
+           CommutativeSquare (a′ ∘ b′) c c″ (a ∘ b)
+sym-glue {a′ = a′} {c′ = c′} {c″ = c″} {a = a} {b′ = b′} {c = c} {b = b} sq-a sq-b = begin
   c″ ∘ (a′ ∘ b′) ≈⟨ pullˡ sq-a ⟩
   (a ∘ c′) ∘ b′  ≈⟨ extendˡ sq-b ⟩
   (a ∘ b) ∘ c    ∎
diff --git a/src/Categories/NaturalTransformation/Core.agda b/src/Categories/NaturalTransformation/Core.agda
index db06af31e..937fbcec6 100644
--- a/src/Categories/NaturalTransformation/Core.agda
+++ b/src/Categories/NaturalTransformation/Core.agda
@@ -83,7 +83,7 @@ _∘ᵥ_ : ∀ {F G H : Functor C D} →
 _∘ᵥ_ {C = C} {D = D} {F} {G} {H} X Y = record
   { η       = λ q → D [ X.η q ∘ Y.η q ]
   ; commute = λ f → glue (X.commute f) (Y.commute f)
-  ; sym-commute = λ f → Category.Equiv.sym D (glue (X.commute f) (Y.commute f))
+  ; sym-commute = λ f → sym-glue (X.sym-commute f) (Y.sym-commute f)
   }
   where module X = NaturalTransformation X
         module Y = NaturalTransformation Y
@@ -92,9 +92,10 @@ _∘ᵥ_ {C = C} {D = D} {F} {G} {H} X Y = record
 -- "Horizontal composition"
 _∘ₕ_ : ∀ {F G : Functor C D} {H I : Functor D E} →
          NaturalTransformation H I → NaturalTransformation F G → NaturalTransformation (H ∘F F) (I ∘F G)
-_∘ₕ_ {E = E} {F} {I = I} Y X = ntHelper record
+_∘ₕ_ {E = E} {F} {I = I} Y X = record
   { η = λ q → E [ I₁ (X.η q) ∘ Y.η (F.F₀ q) ]
   ; commute = λ f → glue ([ I ]-resp-square (X.commute f)) (Y.commute (F.F₁ f))
+  ; sym-commute = λ f → sym-glue ([ I ]-resp-square (X.sym-commute f)) (Y.sym-commute (F.₁ f))
   }
   where module F = Functor F
         module X = NaturalTransformation X
diff --git a/src/Categories/NaturalTransformation/Displayed.agda b/src/Categories/NaturalTransformation/Displayed.agda
new file mode 100644
index 000000000..1dee69954
--- /dev/null
+++ b/src/Categories/NaturalTransformation/Displayed.agda
@@ -0,0 +1,123 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Categories.NaturalTransformation.Displayed where
+
+open import Level
+
+open import Categories.Category.Core
+open import Categories.Category.Displayed
+open import Categories.Functor hiding (id)
+open import Categories.Functor.Displayed renaming (id′ to idF′)
+open import Categories.Functor.Displayed.Properties
+import Categories.Morphism.Displayed.Reasoning as DMR
+open import Categories.NaturalTransformation
+
+private
+  variable
+    o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ o‴ ℓ‴ e‴ : Level
+    C D E : Category o ℓ e
+    F G H : Functor C D
+    C′ D′ : Displayed C o ℓ e
+
+record DisplayedNaturalTransformation
+  {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {F G : Functor C D}
+  {C′ : Displayed C o″ ℓ″ e″} {D′ : Displayed D o‴ ℓ‴ e‴} (F′ : DisplayedFunctor C′ D′ F) (G′ : DisplayedFunctor C′ D′ G)
+  (T : NaturalTransformation F G)
+  : Set (o ⊔ ℓ ⊔ o″ ⊔ ℓ″ ⊔ ℓ‴ ⊔ e‴) where
+  private
+    module C′ = Displayed C′
+    module D′ = Displayed D′
+    module F′ = DisplayedFunctor F′
+    module G′ = DisplayedFunctor G′
+  open NaturalTransformation T
+  field
+    η′ : ∀ {X} (X′ : C′.Obj[ X ]) → F′.₀′ X′ D′.⇒[ η X ] G′.₀′ X′
+    commute′ : ∀ {X Y} {X′ : C′.Obj[ X ]} {Y′ : C′.Obj[ Y ]} {f} (f′ : X′ C′.⇒[ f ] Y′)
+               → η′ Y′ D′.∘′ F′.₁′ f′ D′.≈[ commute f ] G′.₁′ f′ D′.∘′ η′ X′
+    sym-commute′ : ∀ {X Y} {X′ : C′.Obj[ X ]} {Y′ : C′.Obj[ Y ]} {f} (f′ : X′ C′.⇒[ f ] Y′)
+                 → G′.₁′ f′ D′.∘′ η′ X′ D′.≈[ sym-commute f ] η′ Y′ D′.∘′ F′.₁′ f′
+
+  op′ : DisplayedNaturalTransformation G′.op′ F′.op′ op
+  op′ = record
+    { η′ = η′
+    ; commute′ = sym-commute′
+    ; sym-commute′ = commute′
+    }
+
+id′ : ∀ {C′ : Displayed C o″ ℓ″ e″} {D′ : Displayed D o‴ ℓ‴ e‴} {F′ : DisplayedFunctor C′ D′ F}
+      → DisplayedNaturalTransformation F′ F′ id
+id′ {D′ = D′} = record
+  { η′ = λ _ → D′.id′
+  ; commute′ = λ f → id′-comm-sym
+  ; sym-commute′ = λ _ → id′-comm
+  }
+  where
+    module D′ = Displayed D′
+    open DMR D′
+
+_∘′ᵥ_ : ∀ {S : NaturalTransformation G H} {T : NaturalTransformation F G}
+          {C′ : Displayed C o″ ℓ″ e″} {D′ : Displayed D o‴ ℓ‴ e‴}
+          {F′ : DisplayedFunctor C′ D′ F} {G′ : DisplayedFunctor C′ D′ G} {H′ : DisplayedFunctor C′ D′ H}
+        → DisplayedNaturalTransformation G′ H′ S → DisplayedNaturalTransformation F′ G′ T
+        → DisplayedNaturalTransformation F′ H′ (S ∘ᵥ T)
+_∘′ᵥ_ {D′ = D′} S′ T′ = record
+  { η′ = λ X → S′.η′ X D′.∘′ T′.η′ X
+  ; commute′ = λ f → glue′ (S′.commute′ f) (T′.commute′ f)
+  ; sym-commute′ = λ f → sym-glue′ (S′.sym-commute′ f) (T′.sym-commute′ f)
+  }
+  where
+    module D′ = Displayed D′
+    module S′ = DisplayedNaturalTransformation S′
+    module T′ = DisplayedNaturalTransformation T′
+    open DMR D′
+
+_∘′ₕ_ : ∀ {F G : Functor C D} {H I : Functor D E}
+          {S : NaturalTransformation H I} {T : NaturalTransformation F G}
+          {C′ : Displayed C o ℓ e} {D′ : Displayed D o′ ℓ′ e′} {E′ : Displayed E o″ ℓ″ e″}
+          {F′ : DisplayedFunctor C′ D′ F} {G′ : DisplayedFunctor C′ D′ G}
+          {H′ : DisplayedFunctor D′ E′ H} {I′ : DisplayedFunctor D′ E′ I}
+        → DisplayedNaturalTransformation H′ I′ S
+        → DisplayedNaturalTransformation F′ G′ T
+        → DisplayedNaturalTransformation (H′ ∘F′ F′) (I′ ∘F′ G′) (S ∘ₕ T)
+_∘′ₕ_ {E′ = E′} {F′ = F′} {I′ = I′} S′ T′ = record
+  { η′ = λ X → I′.₁′ (T′.η′ X) E′.∘′ S′.η′ (F′.₀′ X)
+  ; commute′ = λ f → glue′ ([ I′ ]-resp-square′ (T′.commute′ f)) (S′.commute′ (F′.₁′ f))
+  ; sym-commute′ = λ f → sym-glue′ ([ I′ ]-resp-square′ (T′.sym-commute′ f)) (S′.sym-commute′ (F′.₁′ f)) 
+  } 
+  where
+    module S′ = DisplayedNaturalTransformation S′
+    module T′ = DisplayedNaturalTransformation T′
+    module E′ = Displayed E′
+    module F′ = DisplayedFunctor F′
+    module I′ = DisplayedFunctor I′
+    open DMR E′
+
+id′∘id′⇒id′ : ∀ {C′ : Displayed C o ℓ e} → DisplayedNaturalTransformation {C′ = C′} {D′ = C′} (idF′ ∘F′ idF′) idF′ id∘id⇒id
+id′∘id′⇒id′ {C′ = C′} = record
+  { η′ = λ _ → Displayed.id′ C′
+  ; commute′ = λ _ → DMR.id′-comm-sym C′
+  ; sym-commute′ = λ _ → DMR.id′-comm C′
+  }
+
+id′⇒id′∘id′ : ∀ {C′ : Displayed C o ℓ e} → DisplayedNaturalTransformation {C′ = C′} {D′ = C′} idF′ (idF′ ∘F′ idF′) id⇒id∘id
+id′⇒id′∘id′ {C′ = C′} = record
+  { η′ = λ _ → Displayed.id′ C′
+  ; commute′ = λ _ → DMR.id′-comm-sym C′
+  ; sym-commute′ = λ _ → DMR.id′-comm C′
+  }
+
+module _ {F′ : DisplayedFunctor C′ D′ F} where
+  open DMR D′
+  private module D′ = Displayed D′
+
+  F′⇒F′∘id′ : DisplayedNaturalTransformation F′ (F′ ∘F′ idF′) F⇒F∘id
+  F′⇒F′∘id′ = record { η′ = λ _ → D′.id′; commute′ = λ _ → id′-comm-sym ; sym-commute′ = λ _ → id′-comm }
+
+  F′⇒id′∘F′ : DisplayedNaturalTransformation F′ (idF′ ∘F′ F′) F⇒id∘F
+  F′⇒id′∘F′ = record { η′ = λ _ → D′.id′ ; commute′ = λ _ → id′-comm-sym ; sym-commute′ = λ _ → id′-comm }
+
+  F′∘id′⇒F′ : DisplayedNaturalTransformation (F′ ∘F′ idF′) F′ F∘id⇒F
+  F′∘id′⇒F′ = record { η′ = λ _ → D′.id′ ; commute′ = λ _ → id′-comm-sym ; sym-commute′ = λ _ → id′-comm }
+
+  id′∘F′⇒F′ : DisplayedNaturalTransformation (idF′ ∘F′ F′) F′ id∘F⇒F
+  id′∘F′⇒F′ = record { η′ = λ _ → D′.id′ ; commute′ = λ _ → id′-comm-sym ; sym-commute′ = λ _ → id′-comm }
diff --git a/src/Categories/NaturalTransformation/NaturalIsomorphism.agda b/src/Categories/NaturalTransformation/NaturalIsomorphism.agda
index b50da9926..f7c1f5985 100644
--- a/src/Categories/NaturalTransformation/NaturalIsomorphism.agda
+++ b/src/Categories/NaturalTransformation/NaturalIsomorphism.agda
@@ -245,10 +245,10 @@ module _ (F : Functor B C) (G : Functor C D) (H : Functor D E) where
   private
     -- components of α
     assocʳ : NaturalTransformation ((H ∘F G) ∘F F) (H ∘F (G ∘F F))
-    assocʳ = ntHelper record { η = λ _ → id ; commute = λ _ → MR.id-comm-sym E  }
+    assocʳ = record { η = λ _ → id ; commute = λ _ → MR.id-comm-sym E ; sym-commute = λ _ → MR.id-comm E }
 
     assocˡ : NaturalTransformation (H ∘F (G ∘F F)) ((H ∘F G) ∘F F)
-    assocˡ = ntHelper record { η = λ _ → id ; commute = λ _ → MR.id-comm-sym E }
+    assocˡ = record { η = λ _ → id ; commute = λ _ → MR.id-comm-sym E ; sym-commute = λ _ → MR.id-comm E }
 
   associator : (H ∘F G) ∘F F ≃ H ∘F (G ∘F F)
   associator = record { F⇒G = assocʳ ; F⇐G = assocˡ ; iso = iso-id-id }
diff --git a/src/Categories/NaturalTransformation/NaturalIsomorphism/Displayed.agda b/src/Categories/NaturalTransformation/NaturalIsomorphism/Displayed.agda
new file mode 100644
index 000000000..4adb91381
--- /dev/null
+++ b/src/Categories/NaturalTransformation/NaturalIsomorphism/Displayed.agda
@@ -0,0 +1,159 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Categories.NaturalTransformation.NaturalIsomorphism.Displayed where
+
+open import Level
+open import Relation.Binary.Displayed
+
+open import Categories.Category
+open import Categories.Category.Displayed
+open import Categories.Functor
+open import Categories.Functor.Displayed renaming (id′ to idF′)
+open import Categories.Functor.Displayed.Properties
+import Categories.Morphism.Displayed as DMorphism
+import Categories.Morphism.Displayed.Properties as DMorphismₚ
+import Categories.Morphism.Displayed.Reasoning as DMR
+open import Categories.NaturalTransformation.Displayed as DNT hiding (id′)
+open import Categories.NaturalTransformation.NaturalIsomorphism
+
+private
+  variable
+    bo bℓ be bo′ bℓ′ be′ bo″ bℓ″ be″ o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ o‴ ℓ‴ e‴ : Level
+    B C D E : Category o ℓ e
+    F G H I : Functor C D
+    C′ : Displayed C o ℓ e
+    D′ : Displayed D o ℓ e
+    E′ : Displayed E o ℓ e
+
+record DisplayedNaturalIsomorphism
+  {C′ : Displayed C o ℓ e} {D′ : Displayed D o′ ℓ′ e′}
+  (F′ : DisplayedFunctor C′ D′ F) (G′ : DisplayedFunctor C′ D′ G)
+  (F≃G : NaturalIsomorphism F G)
+  : Set (Category.o-level C ⊔ Category.ℓ-level C ⊔ o ⊔ ℓ ⊔ ℓ′ ⊔ e′) where
+  open Displayed C′
+  open NaturalIsomorphism F≃G
+  field
+    F′⇒G′ : DisplayedNaturalTransformation F′ G′ F⇒G
+    F′⇐G′ : DisplayedNaturalTransformation G′ F′ F⇐G
+
+  module ⇒′ = DisplayedNaturalTransformation F′⇒G′
+  module ⇐′ = DisplayedNaturalTransformation F′⇐G′
+
+  field
+    iso′ : ∀ {X} (X′ : Obj[ X ])  → DMorphism.DisplayedIso D′ (⇒′.η′ X′) (⇐′.η′ X′) (iso X)
+
+  module iso′ {X} (X′ : Obj[ X ]) = DMorphism.DisplayedIso (iso′ X′)
+
+open DisplayedNaturalIsomorphism
+
+infix 4 _≃[_]_
+
+_≃[_]_ : ∀ (F′ : DisplayedFunctor C′ D′ F) (F≃G : NaturalIsomorphism F G) (G′ : DisplayedFunctor C′ D′ G) → Set _
+F′ ≃[ F≃G ] G′ = DisplayedNaturalIsomorphism F′ G′ F≃G
+
+_ⓘᵥ′_ : ∀ {F′ : DisplayedFunctor C′ D′ F} {G′ : DisplayedFunctor C′ D′ G} {H′ : DisplayedFunctor C′ D′ H} {G≃H} {F≃G}
+        → G′ ≃[ G≃H ] H′ → F′ ≃[ F≃G ] G′ → F′ ≃[ G≃H ⓘᵥ F≃G ] H′
+_ⓘᵥ′_ {D′ = D′} G′≃H′ F′≃G′ = record
+  { F′⇒G′ = F′⇒G′ G′≃H′ ∘′ᵥ F′⇒G′ F′≃G′
+  ; F′⇐G′ = F′⇐G′ F′≃G′ ∘′ᵥ F′⇐G′ G′≃H′
+  ; iso′ = λ X → DisplayedIso-∘′ (iso′ F′≃G′ X) (iso′ G′≃H′ X)
+  }
+  where
+    open DMorphismₚ D′
+
+_ⓘₕ′_ : ∀ {C : Category bo bℓ be} {D : Category bo′ bℓ′ be′} {E : Category bo″ bℓ″ be″}
+          {H I : Functor D E} {F G : Functor C D}
+          {C′ : Displayed C o ℓ e} {D′ : Displayed D o′ ℓ′ e′} {E′ : Displayed E o″ ℓ″ e″}
+          {H′ : DisplayedFunctor D′ E′ H} {I′ : DisplayedFunctor D′ E′ I}
+          {F′ : DisplayedFunctor C′ D′ F} {G′ : DisplayedFunctor C′ D′ G}
+          {H≃I} {F≃G}
+      → H′ ≃[ H≃I ] I′ → F′ ≃[ F≃G ] G′ → (H′ ∘F′ F′) ≃[ H≃I ⓘₕ F≃G ] (I′ ∘F′ G′)
+_ⓘₕ′_ {E′ = E′} {I′ = I′} H′≃I′ F′≃G′ = record
+  { F′⇒G′ = F′⇒G′ H′≃I′ ∘′ₕ F′⇒G′ F′≃G′
+  ; F′⇐G′ = F′⇐G′ H′≃I′ ∘′ₕ F′⇐G′ F′≃G′
+  ; iso′ = λ X′ → DisplayedIso-resp-≈[] (DisplayedIso-∘′ (iso′ H′≃I′ _) ([ I′ ]-resp-DisplayedIso (iso′ F′≃G′ X′))) Equiv′.refl′ (⇐′.commute′ H′≃I′ (⇐′.η′ F′≃G′ X′))
+  }
+  where
+    open Displayed E′
+    open DMorphismₚ E′
+
+refl′ : ∀ {F′ : DisplayedFunctor C′ D′ F} → F′ ≃[ refl ] F′
+refl′ {D′ = D′} = record
+  { F′⇒G′ = DNT.id′
+  ; F′⇐G′ = DNT.id′
+  ; iso′ = λ X′ → record
+    { isoˡ′ = Displayed.identityˡ′ D′
+    ; isoʳ′ = Displayed.identityʳ′ D′
+    }
+  }
+
+sym′ : ∀ {F′ : DisplayedFunctor C′ D′ F} {G′ : DisplayedFunctor C′ D′ G} {F≃G}
+       → F′ ≃[ F≃G ] G′ → G′ ≃[ sym F≃G ] F′
+sym′ F′≃G′ = record
+  { F′⇒G′ = F′⇐G′ F′≃G′
+  ; F′⇐G′ = F′⇒G′ F′≃G′
+  ; iso′ = λ X′ →
+    let open DMorphism.DisplayedIso (iso′ F′≃G′ X′) in record
+    { isoˡ′ = isoʳ′
+    ; isoʳ′ = isoˡ′
+    }
+  }
+
+trans′ : ∀ {F′ : DisplayedFunctor C′ D′ F} {G′ : DisplayedFunctor C′ D′ G} {H′ : DisplayedFunctor C′ D′ H} {F≃G} {G≃H}
+         → F′ ≃[ F≃G ] G′ → G′ ≃[ G≃H ] H′ → F′ ≃[ trans F≃G G≃H ] H′
+trans′ F′≃G′ G′≃H′ = G′≃H′ ⓘᵥ′ F′≃G′
+
+isDisplayedEquivalence : {C′ : Displayed C o ℓ e} {D′ : Displayed D o′ ℓ′ e′}
+                       → IsDisplayedEquivalence isEquivalence (_≃[_]_ {C′ = C′} {D′ = D′})
+isDisplayedEquivalence = record { refl′ = refl′ ; sym′ = sym′ ; trans′ = trans′ }
+
+module LeftRightId′ (F′ : DisplayedFunctor C′ D′ F) where
+  open LeftRightId F
+  module D′ = Displayed D′
+
+  iso-id′-id′ : ∀ {X} (X′ : Displayed.Obj[_] C′ X) → DMorphism.DisplayedIso D′ {X′ = DisplayedFunctor.F₀′ F′ X′} D′.id′ D′.id′ (iso-id-id X)
+  iso-id′-id′ X′ = record { isoˡ′ = D′.identityˡ′ ; isoʳ′ = D′.identityʳ′ }
+
+-- unitors
+module _ {F : Functor C D} {F′ : DisplayedFunctor C′ D′ F} where
+  open LeftRightId′ F′
+  
+  unitorˡ′ : idF′ ∘F′ F′ ≃[ unitorˡ ] F′
+  unitorˡ′ = record { F′⇒G′ = id′∘F′⇒F′ ; F′⇐G′ = F′⇒id′∘F′ ; iso′ = iso-id′-id′ }
+
+  unitorʳ′ : F′ ∘F′ idF′ ≃[ unitorʳ ] F′
+  unitorʳ′ = record { F′⇒G′ = F′∘id′⇒F′ ; F′⇐G′ = F′⇒F′∘id′ ; iso′ = iso-id′-id′ }
+
+unitor²′ : ∀ {C′ : Displayed C o ℓ e} → idF′ ∘F′ idF′ ≃[ unitor² ] idF′ {C = C′}
+unitor²′ = record { F′⇒G′ = id′∘id′⇒id′ ; F′⇐G′ = id′⇒id′∘id′ ; iso′ = LeftRightId′.iso-id′-id′ idF′ }
+
+-- associator
+module _
+  {F : Functor B C} {G : Functor C D} {H : Functor D E}
+  {B′ : Displayed B o ℓ e} {C′ : Displayed C o′ ℓ′ e′} {D′ : Displayed D o″ ℓ″ e″} {E′ : Displayed E o‴ ℓ‴ e‴}
+  (F′ : DisplayedFunctor B′ C′ F) (G′ : DisplayedFunctor C′ D′ G) (H′ : DisplayedFunctor D′ E′ H)
+  where
+
+  open Displayed E′
+  open LeftRightId′ (H′ ∘F′ (G′ ∘F′ F′))
+
+  private
+    assocʳ′ : DisplayedNaturalTransformation ((H′ ∘F′ G′) ∘F′ F′) (H′ ∘F′ (G′ ∘F′ F′)) _
+    assocʳ′ = record
+      { η′ = λ _ → id′
+      ; commute′ = λ _ → DMR.id′-comm-sym E′
+      ; sym-commute′ = λ _ → DMR.id′-comm E′
+      }
+
+    assocˡ′ : DisplayedNaturalTransformation (H′ ∘F′ (G′ ∘F′ F′)) ((H′ ∘F′ G′) ∘F′ F′) _
+    assocˡ′ = record
+      { η′ = λ _ → id′
+      ; commute′ = λ _ → DMR.id′-comm-sym E′
+      ; sym-commute′ = λ _ → DMR.id′-comm E′
+      }
+
+  associator′ : (H′ ∘F′ G′) ∘F′ F′ ≃[ associator F G H ] H′ ∘F′ (G′ ∘F′ F′)
+  associator′ = record { F′⇒G′ = assocʳ′ ; F′⇐G′ = assocˡ′ ; iso′ = iso-id′-id′ }
+
+  sym-associator′ : H′ ∘F′ (G′ ∘F′ F′) ≃[ sym-associator F G H ] (H′ ∘F′ G′) ∘F′ F′
+  sym-associator′ = record { F′⇒G′ = assocˡ′ ; F′⇐G′ = assocʳ′ ; iso′ = iso-id′-id′ }
diff --git a/src/Relation/Binary/Displayed.agda b/src/Relation/Binary/Displayed.agda
new file mode 100644
index 000000000..35c39c2cc
--- /dev/null
+++ b/src/Relation/Binary/Displayed.agda
@@ -0,0 +1,30 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Relation.Binary.Displayed where
+
+open import Level using (Level; suc; _⊔_)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Structures using (IsEquivalence)
+
+private
+  variable
+    a ℓ a′ ℓ′ : Level
+
+record IsDisplayedEquivalence
+  {A : Set a} {_≈_ : Rel A ℓ} (isEquivalence : IsEquivalence _≈_)
+  {A′ : A → Set a′} (_≈[_]_ : ∀ {x y} → A′ x → x ≈ y → A′ y → Set ℓ′) : Set (a ⊔ ℓ ⊔ a′ ⊔ ℓ′)
+  where
+  open IsEquivalence isEquivalence
+  field
+    refl′ : ∀ {x} {x′ : A′ x} → x′ ≈[ refl ] x′
+    sym′ : ∀ {x y} {x′ : A′ x} {y′ : A′ y} {p : x ≈ y} → x′ ≈[ p ] y′ → y′ ≈[ sym p ] x′
+    trans′ : ∀ {x y z} {x′ : A′ x} {y′ : A′ y} {z′ : A′ z} {p : x ≈ y} {q : y ≈ z} → x′ ≈[ p ] y′ → y′ ≈[ q ] z′ → x′ ≈[ trans p q ] z′
+
+record DisplayedSetoid (B : Setoid a ℓ) a′ ℓ′ : Set (a ⊔ ℓ ⊔ suc (a′ ⊔ ℓ′)) where
+  open Setoid B
+  field
+    Carrier′ : Carrier → Set a′
+    _≈[_]_ : ∀ {x y} → Carrier′ x → x ≈ y → Carrier′ y → Set ℓ′
+    isDisplayedEquivalence : IsDisplayedEquivalence isEquivalence _≈[_]_
+  open IsDisplayedEquivalence isDisplayedEquivalence public
diff --git a/src/Relation/Binary/Displayed/Reasoning/Setoid.agda b/src/Relation/Binary/Displayed/Reasoning/Setoid.agda
new file mode 100644
index 000000000..1ea45a378
--- /dev/null
+++ b/src/Relation/Binary/Displayed/Reasoning/Setoid.agda
@@ -0,0 +1,41 @@
+{-# OPTIONS --safe --without-K #-}
+
+open import Relation.Binary
+open import Relation.Binary.Displayed
+
+module Relation.Binary.Displayed.Reasoning.Setoid {a ℓ a′ ℓ′} {S : Setoid a ℓ} (S′ : DisplayedSetoid S a′ ℓ′) where
+
+open import Level
+open import Relation.Binary.Reasoning.Setoid S
+
+open Setoid S
+open DisplayedSetoid S′
+
+infix 4 _IsRelatedTo[_]_
+
+data _IsRelatedTo[_]_ {x y : Carrier} (x′ : Carrier′ x) (p : x IsRelatedTo y) (y′ : Carrier′ y) : Set (ℓ ⊔ ℓ′) where
+  relTo[] : (x′≈[x≈y]y′ : x′ ≈[ begin p ] y′) → x′ IsRelatedTo[ p ] y′
+
+infix  1 begin′_
+infixr 2 step-≈[] step-≈˘[]
+infix  4 _∎′
+
+begin′_ : ∀ {x y} {x′ : Carrier′ x} {y′ : Carrier′ y} {x∼y : x IsRelatedTo y}
+          → x′ IsRelatedTo[ x∼y ] y′ → x′ ≈[ begin x∼y ] y′
+begin′ relTo[] x′≈[x≈y]y′ = x′≈[x≈y]y′
+
+step-≈[] : ∀ {x y z} (x′ : Carrier′ x) {y′ : Carrier′ y} {z′ : Carrier′ z} {y∼z : y IsRelatedTo z} {x≈y : x ≈ y}
+         → y′ IsRelatedTo[ y∼z ] z′ → x′ ≈[ x≈y ] y′ → x′ IsRelatedTo[ step-≈ x y∼z x≈y ] z′
+step-≈[] x′ {y∼z = relTo _} (relTo[] y≈[]z) x≈[]y = relTo[] (trans′ x≈[]y y≈[]z)
+syntax step-≈[] x′ y′∼z′ x′≈[]y′ = x′ ≈[]⟨ x′≈[]y′ ⟩ y′∼z′
+
+step-≈˘[] : ∀ {x y z} (x′ : Carrier′ x) {y′ : Carrier′ y} {z′ : Carrier′ z} {y∼z : y IsRelatedTo z} {y≈x : y ≈ x}
+          → y′ IsRelatedTo[ y∼z ] z′ → y′ ≈[ y≈x ] x′ → x′ IsRelatedTo[ step-≈˘ x y∼z y≈x ] z′
+step-≈˘[] x′ y′∼z′ y′≈x′ = x′ ≈[]⟨ sym′ y′≈x′ ⟩ y′∼z′ 
+syntax step-≈˘[] x′ y′∼z′ y′≈[]x′ = x′ ≈˘[]⟨ y′≈[]x′ ⟩ y′∼z′
+
+_∎′ : ∀ {x} (x′ : Carrier′ x) → x′ IsRelatedTo[ x ∎ ] x′
+_∎′ x′ = relTo[] refl′
+
+-- TODO: propositional equality
+-- Maybe TODO: have a convenient way to specify the base equality, e.g. _≈[_]⟨_⟩_