diff --git a/src/Cat/Bi/Base.lagda.md b/src/Cat/Bi/Base.lagda.md
index 602b91e2d..ae18a217d 100644
--- a/src/Cat/Bi/Base.lagda.md
+++ b/src/Cat/Bi/Base.lagda.md
@@ -190,6 +190,8 @@ naturally isomorphic to the identity functor.
         (compose-assocˡ {H = Hom} compose)
         (compose-assocʳ {H = Hom} compose)
 
+  module unitor-l {a} {b} = Cr._≅_ _ (unitor-l {a} {b})
+  module unitor-r {a} {b} = Cr._≅_ _ (unitor-r {a} {b})
   module associator {a} {b} {c} {d} = Cr._≅_ _ (associator {a} {b} {c} {d})
 ```
 
diff --git a/src/Cat/Bi/Displayed/Base.lagda.md b/src/Cat/Bi/Displayed/Base.lagda.md
new file mode 100644
index 000000000..83dbf6e0d
--- /dev/null
+++ b/src/Cat/Bi/Displayed/Base.lagda.md
@@ -0,0 +1,362 @@
+<!--
+```agda
+open import Cat.Displayed.Instances.DisplayedFunctor hiding (_◆'_)
+open import Cat.Displayed.Instances.TotalProduct
+open import Cat.Displayed.Functor.Naturality
+open import Cat.Displayed.Morphism
+open import Cat.Displayed.Functor
+open import Cat.Instances.Product
+open import Cat.Displayed.Total
+open import Cat.Displayed.Base
+open import Cat.Bi.Base
+open import Cat.Prelude
+
+import Cat.Displayed.Reasoning as DR
+```
+-->
+```agda
+module Cat.Bi.Displayed.Base where
+```
+
+# Displayed bicategories {defines=displayed-bicategory}
+
+::: source
+The definition here was adapted from the one given by Ahrens et al. [-@Ahrens-Frumin-Maggesi-Veltre-vanDerWeide:Bicategories]
+:::
+
+Just as a displayed category $\cE \liesover \cB$ allows us to describe categorical structure over the category $\cB$, a
+**displayed bicategory** $\bf{E} \liesover \bf{B}$ allows us to describe *bi*categorical structure over the *bi*category $\bf{B}$.
+
+<!--
+```agda
+open Functor
+open Displayed-functor
+open _=[_]=>_
+open make-natural-iso[_]
+
+module _ where
+ 
+  compose-assocˡ' : ∀ {o o' d d' ℓ ℓ'} {O : Type o} {H : O → O → Precategory ℓ ℓ'}
+                  → {O' : O → Type o'} {H' : ∀ {a b} → O' a → O' b → Displayed (H a b) d d'}
+                  → {F : ∀ {A B C} → Functor (H B C ×ᶜ H A B) (H A C)}
+                  → (F' : ∀ {A B C} {A' : O' A} {B' : O' B} {C' : O' C} → Displayed-functor F (H' B' C' ×ᵀᴰ H' A' B') (H' A' C'))
+                  → ∀ {A B C D} {A' : O' A} {B' : O' B} {C' : O' C} {D' : O' D} 
+                  → Displayed-functor (compose-assocˡ {O = O} {H = H} F) (H' C' D' ×ᵀᴰ H' B' C' ×ᵀᴰ H' A' B') (H' A' D')
+  compose-assocˡ' F' .F₀' (F , G , H) = F' .F₀' (F' .F₀' (F , G) , H)
+  compose-assocˡ' F' .F₁' (f , g , h) = F' .F₁' (F' .F₁' (f , g) , h)
+  compose-assocˡ' {H' = H'} F' {A' = A'} {D' = D'} .F-id' = 
+    cast[] (apd (λ _ → F' .F₁') (F' .F-id' ,ₚ refl) ∙[] (F' .F-id')) 
+    where 
+      open DR (H' A' D')
+  compose-assocˡ' {H' = H'} F' {A' = A'} {D' = D'} .F-∘' = 
+    cast[] (apd (λ _ → F' .F₁') (F' .F-∘' ,ₚ refl) ∙[] F' .F-∘')
+    where 
+      open DR (H' A' D')
+
+  compose-assocʳ' : ∀ {o o' d d' ℓ ℓ'} {O : Type o} {H : O → O → Precategory ℓ ℓ'}
+                   → {O' : O → Type o'} {H' : ∀ {a b} → O' a → O' b → Displayed (H a b) d d'}
+                   → {F : ∀ {A B C} → Functor (H B C ×ᶜ H A B) (H A C)}
+                   → (F' : ∀ {A B C} {A' : O' A} {B' : O' B} {C' : O' C}
+                         → Displayed-functor F (H' B' C' ×ᵀᴰ H' A' B') (H' A' C'))
+                   → ∀ {A B C D} {A' : O' A} {B' : O' B} {C' : O' C} {D' : O' D}
+                   → Displayed-functor (compose-assocʳ {O = O} {H = H} F)
+                                       (H' C' D' ×ᵀᴰ H' B' C' ×ᵀᴰ H' A' B') (H' A' D')
+  compose-assocʳ' F' .F₀' (F , G , H) = F' .F₀' (F , F' .F₀' (G , H))
+  compose-assocʳ' F' .F₁' (f , g , h) = F' .F₁' (f , F' .F₁' (g , h))
+  compose-assocʳ' {H' = H'} F' {A' = A'} {D' = D'} .F-id' =
+    cast[] (apd (λ _ → F' .F₁') (refl ,ₚ F' .F-id') ∙[] F' .F-id')
+    where
+      open DR (H' A' D')
+  compose-assocʳ' {H' = H'} F' {A' = A'} {D' = D'} .F-∘' =
+    cast[] (apd (λ _ → F' .F₁') (refl ,ₚ F' .F-∘') ∙[] F' .F-∘')
+    where
+      open DR (H' A' D')
+```
+-->
+
+```agda
+record Bidisplayed {o oh ℓh} (B : Prebicategory o oh ℓh) o' oh' ℓh' : Type (lsuc (o' ⊔ oh' ⊔ ℓh') ⊔ o ⊔ oh ⊔ ℓh) where
+  no-eta-equality
+  open Prebicategory B
+```
+
+For each object of the base bicateogry, we have a type of displayed objects indexed over it.
+
+```agda
+  field
+    Ob[_] : Ob → Type o'
+```
+
+For any two displayed objects, we have a category displayed over the $\hom$ category of their bases.
+
+```agda
+    Hom[_,_] : ∀ {A B} → Ob[ A ] → Ob[ B ] → Displayed (Hom A B) oh' ℓh'
+
+  module Hom[] {A B} {A' : Ob[ A ]} {B' : Ob[ B ]} = Displayed (Hom[ A' , B' ])
+```
+
+The displayed objects of these displayed $\hom$ categories are the _displayed 1-cells_.
+The displayed morphims are the _displayed 2-cells_.
+
+```agda
+  _[_]↦_ : ∀ {A B} → Ob[ A ] → (A ↦ B) → Ob[ B ] → Type _
+  A' [ f ]↦ B' = Hom[ A' , B' ] .Displayed.Ob[_] f
+
+
+  _[_]⇒_ : ∀ {A B} {f g : A ↦ B} 
+         → {A' : Ob[ A ]} {B' : Ob[ B ]} 
+         → A' [ f ]↦ B' → (f ⇒ g) → A' [ g ]↦ B'
+         → Type _
+  _[_]⇒_ {A' = A'} {B' = B'} f' α g' = Hom[ A' , B' ] .Displayed.Hom[_] α f' g'
+```
+
+We require an identity 1-cell displayed over the identity 1-cell of the base bicategory.
+
+```agda 
+  field
+    ↦id' : ∀ {x} {x' : Ob[ x ]} → x' [ id ]↦ x'
+```
+
+We get displayed identity 2-cells automatically from the displayed $\hom$ structure.
+
+```agda 
+  ⇒id' : ∀ {A B} {A' : Ob[ A ]} {B' : Ob[ B ]}
+      → {f : A ↦ B} {f' : A' [ f ]↦ B'}
+      → f' [ Hom.id ]⇒ f'
+  ⇒id' = Hom[].id'
+```
+
+The displayed composition functor is between total products of displayed $\hom$ categories, and
+lies over the composition functor of the base bicategory.
+
+```agda
+  field
+    compose' : ∀ {A B C} {A' : Ob[ A ]} {B' : Ob[ B ]} {C' : Ob[ C ]} 
+             → Displayed-functor compose (Hom[ B' , C' ] ×ᵀᴰ Hom[ A' , B' ]) Hom[ A' , C' ]
+    
+  module compose' {A} {B} {C} {A'} {B'} {C'} = Displayed-functor (compose' {A} {B} {C} {A'} {B'} {C'})
+```
+
+Displayed 1-cell and 2-cell composition proceeds in the same way.
+
+```agda 
+  _⊗'_ : ∀ {A B C A' B' C'} {f : B ↦ C} {g : A ↦ B} → (B' [ f ]↦ C') → (A' [ g ]↦ B') → A' [ f ⊗ g ]↦ C'
+  _⊗'_ f' g' = compose'.₀' (f' , g') 
+
+  _∘'_ : ∀ {A B A' B'} {f g h : A ↦ B} 
+      → {f' : A' [ f ]↦ B'} {g' : A' [ g ]↦ B'} {h' : A' [ h ]↦ B'}
+      → {β : g ⇒ h} {α : f ⇒ g} 
+      → g' [ β ]⇒ h' → f' [ α ]⇒ g'
+      → f' [ β ∘ α ]⇒ h'
+  _∘'_ = Hom[]._∘'_
+
+  _◆'_ : ∀ {A B C A' B' C'} 
+       → {f₁ f₂ : B ↦ C} {β : f₁ ⇒ f₂} 
+       → {g₁ g₂ : A ↦ B} {α : g₁ ⇒ g₂}
+       → {f₁' : B' [ f₁ ]↦ C'} {f₂' : B' [ f₂ ]↦ C'}
+       → {g₁' : A' [ g₁ ]↦ B'} {g₂' : A' [ g₂ ]↦ B'}
+       → (β' : f₁' [ β ]⇒ f₂') (α' : g₁' [ α ]⇒ g₂')
+       → (f₁' ⊗' g₁') [ β ◆ α ]⇒ (f₂' ⊗' g₂') 
+  _◆'_ α' β' = compose'.₁' (α' , β')
+
+  infixr 30 _∘'_
+  infixr 25 _⊗'_
+  infix 35 _◀'_ _▶'_
+
+  _▶'_ : ∀ {A B C A' B' C'} {f : B ↦ C} {g₁ g₂ : A ↦ B} {α : g₁ ⇒ g₂}
+        → {g₁' : A' [ g₁ ]↦ B'} {g₂' : A' [ g₂ ]↦ B'} 
+        → (f' : B' [ f ]↦ C')
+        → (α' : g₁' [ α ]⇒ g₂')
+        → f' ⊗' g₁' [ f ▶ α ]⇒ f' ⊗' g₂'
+  _▶'_ f' α' = compose'.₁' (⇒id' , α')
+
+
+  _◀'_ : ∀ {A B C A' B' C'} {g : A ↦ B} {f₁ f₂ : B ↦ C} {β : f₁ ⇒ f₂}
+        → {f₁' : B' [ f₁ ]↦ C'} {f₂' : B' [ f₂ ]↦ C'} 
+        → (β' : f₁' [ β ]⇒ f₂')
+        → (g' : A' [ g ]↦ B')
+        → f₁' ⊗' g' [ β ◀ g ]⇒ f₂' ⊗' g'
+  _◀'_ β' g' = compose'.₁' (β' , ⇒id')
+
+```
+
+The unitors and associator are displayed isomorphims over the unitors and associator the base bicategory.
+
+```agda 
+  field
+    unitor-l' : ∀ {A B} {A' : Ob[ A ]} {B' : Ob[ B ]} → Id' {ℰ = Hom[ A' , B' ]} ≅[ unitor-l ]ⁿ (Right' compose' ↦id')
+    unitor-r' : ∀ {A B} {A' : Ob[ A ]} {B' : Ob[ B ]} → Id' {ℰ = Hom[ A' , B' ]} ≅[ unitor-r ]ⁿ (Left'  compose' ↦id')
+
+    associator' : ∀ {A B C D} {A' : Ob[ A ]} {B' : Ob[ B ]} {C' : Ob[ C ]} {D' : Ob[ D ]}
+                → _≅[_]_ Disp[ Hom[ C' , D' ] ×ᵀᴰ (Hom[ B' , C' ] ×ᵀᴰ Hom[ A' , B' ]) , Hom[ A' , D' ] ] 
+                  (compose-assocˡ' {H' = Hom[_,_]}  compose') associator (compose-assocʳ' {H' = Hom[_,_]}  compose')
+    
+  module unitor-l' {A} {B} {A'} {B'} = _≅[_]_ (unitor-l' {A} {B} {A'} {B'})
+  module unitor-r' {A} {B} {A'} {B'} = _≅[_]_ (unitor-r' {A} {B} {A'} {B'})
+  module associator' {A} {B} {C} {D} {A'} {B'} {C'} {D'} = _≅[_]_ (associator' {A} {B} {C} {D} {A'} {B'} {C'} {D'})
+
+      
+```
+
+The associated displayed cell combinators proceed in the same way.
+
+```agda
+  λ←' : ∀ {A B A' B'} {f : A ↦ B} (f' : A' [ f ]↦ B') → (↦id' ⊗' f') [ λ← f ]⇒ f'
+  λ←' = unitor-l'.from' .η' 
+
+  λ→' : ∀ {A B A' B'} {f : A ↦ B}
+       → (f' : A' [ f ]↦ B')
+       → f' [ λ→ f ]⇒ (↦id' ⊗' f')
+  λ→' = unitor-l'.to' .η'
+
+  ρ←' : ∀ {A B A' B'} {f : A ↦ B}
+       → (f' : A' [ f ]↦ B')
+       → (f' ⊗' ↦id') [ ρ← f ]⇒ f'
+  ρ←' = unitor-r'.from' .η'
+
+  ρ→' : ∀ {A B A' B'} {f : A ↦ B}
+       → (f' : A' [ f ]↦ B')
+       → f' [ ρ→ f ]⇒ (f' ⊗' ↦id')
+  ρ→' = unitor-r'.to' .η'
+
+  ρ←nat' : ∀ {A B A' B'} {f₁ f₂ : A ↦ B} {β : f₁ ⇒ f₂}
+         → {f₁' : A' [ f₁ ]↦ B'} {f₂' : A' [ f₂ ]↦ B'}
+         → (β' : f₁' [ β ]⇒ f₂')
+         → (ρ←' _ ∘' (β' ◀' ↦id')) Hom[].≡[ ρ←nat β ] (β' ∘' ρ←' _)
+  ρ←nat' β' = unitor-r'.from' .is-natural' _ _ β'
+
+  λ←nat' : ∀ {A B A' B'} {f₁ f₂ : A ↦ B} {β : f₁ ⇒ f₂}
+         → {f₁' : A' [ f₁ ]↦ B'} {f₂' : A' [ f₂ ]↦ B'}
+         → (β' : f₁' [ β ]⇒ f₂')
+         → (λ←' _ ∘' (↦id' ▶' β')) Hom[].≡[ λ←nat β ] (β' ∘' λ←' _)
+  λ←nat' β' = unitor-l'.from' .is-natural' _ _ β'
+
+  ρ→nat' : ∀ {A B A' B'} {f₁ f₂ : A ↦ B} {β : f₁ ⇒ f₂}
+         → {f₁' : A' [ f₁ ]↦ B'} {f₂' : A' [ f₂ ]↦ B'}
+         → (β' : f₁' [ β ]⇒ f₂')
+         → (ρ→' _ ∘' β') Hom[].≡[ ρ→nat β ] ((β' ◀' ↦id') ∘' ρ→' _)
+  ρ→nat' β' = unitor-r'.to' .is-natural' _ _ β'
+
+  λ→nat' : ∀ {A B A' B'} {f₁ f₂ : A ↦ B} {β : f₁ ⇒ f₂}
+         → {f₁' : A' [ f₁ ]↦ B'} {f₂' : A' [ f₂ ]↦ B'}
+         → (β' : f₁' [ β ]⇒ f₂')
+         → (λ→' _ ∘' β') Hom[].≡[ λ→nat β ] ((↦id' ▶' β') ∘' λ→' _)
+  λ→nat' β' = unitor-l'.to' .is-natural' _ _ β'
+
+  α→' : ∀ {A B C D A' B' C' D'}
+       {f : C ↦ D} {g : B ↦ C} {h : A ↦ B}
+       → (f' : C' [ f ]↦ D') (g' : B' [ g ]↦ C') (h' : A' [ h ]↦ B')
+       → ((f' ⊗' g') ⊗' h') [ α→ f g h ]⇒ (f' ⊗' (g' ⊗' h'))
+  α→' f' g' h' = associator'.to' .η' (f' , g' , h')
+
+  α←' : ∀ {A B C D A' B' C' D'}
+       {f : C ↦ D} {g : B ↦ C} {h : A ↦ B}
+       → (f' : C' [ f ]↦ D') (g' : B' [ g ]↦ C') (h' : A' [ h ]↦ B')
+       → (f' ⊗' (g' ⊗' h')) [ α← f g h ]⇒ ((f' ⊗' g') ⊗' h')
+  α←' f' g' h' = associator'.from' .η' (f' , g' , h')
+
+  α←nat' : ∀ {A B C D A' B' C' D'}
+         {f₁ f₂ : C ↦ D} {g₁ g₂ : B ↦ C} {h₁ h₂ : A ↦ B}
+         {β : f₁ ⇒ f₂} {γ : g₁ ⇒ g₂} {δ : h₁ ⇒ h₂}
+         {f₁' : C' [ f₁ ]↦ D'} {f₂' : C' [ f₂ ]↦ D'}
+         {g₁' : B' [ g₁ ]↦ C'} {g₂' : B' [ g₂ ]↦ C'}
+         {h₁' : A' [ h₁ ]↦ B'} {h₂' : A' [ h₂ ]↦ B'}
+         → (β' : f₁' [ β ]⇒ f₂') (γ' : g₁' [ γ ]⇒ g₂') (δ' : h₁' [ δ ]⇒ h₂')
+         → (α←' _ _ _ ∘' (β' ◆' (γ' ◆' δ'))) Hom[].≡[ α←nat β γ δ ]
+              (((β' ◆' γ') ◆' δ') ∘' α←' _ _ _)
+  α←nat' β' γ' δ' =
+    associator'.from' .is-natural' (_ , _ , _) (_ , _ , _) (β' , γ' , δ')
+
+  α→nat' : ∀ {A B C D A' B' C' D'}
+         {f₁ f₂ : C ↦ D} {g₁ g₂ : B ↦ C} {h₁ h₂ : A ↦ B}
+         {β : f₁ ⇒ f₂} {γ : g₁ ⇒ g₂} {δ : h₁ ⇒ h₂}
+         {f₁' : C' [ f₁ ]↦ D'} {f₂' : C' [ f₂ ]↦ D'}
+         {g₁' : B' [ g₁ ]↦ C'} {g₂' : B' [ g₂ ]↦ C'}
+         {h₁' : A' [ h₁ ]↦ B'} {h₂' : A' [ h₂ ]↦ B'}
+         → (β' : f₁' [ β ]⇒ f₂') (γ' : g₁' [ γ ]⇒ g₂') (δ' : h₁' [ δ ]⇒ h₂')
+         → (α→' _ _ _ ∘' ((β' ◆' γ') ◆' δ')) Hom[].≡[ α→nat β γ δ ]
+              ((β' ◆' (γ' ◆' δ')) ∘' α→' _ _ _)
+  α→nat' β' γ' δ' =
+    associator'.to' .is-natural' (_ , _ , _) (_ , _ , _) (β' , γ' , δ')
+```
+
+As do the triangle and pentagon identities.
+
+```agda
+  field
+    triangle' 
+      : ∀ {A B C A' B' C'} {f : B ↦ C} {g : A ↦ B}
+      → (f' : B' [ f ]↦ C') (g' : A' [ g ]↦ B')
+      → ((ρ←' f' ◀' g') ∘' α←' f' ↦id' g') Hom[].≡[ triangle f g ] (f' ▶' λ←' g')
+
+    pentagon'
+      : ∀ {A B C D E A' B' C' D' E'}
+      → {f : D ↦ E} {g : C ↦ D} {h : B ↦ C} {i : A ↦ B}
+      → (f' : D' [ f ]↦ E')
+      → (g' : C' [ g ]↦ D')
+      → (h' : B' [ h ]↦ C')
+      → (i' : A' [ i ]↦ B')
+      → ((α←' f' g' h' ◀' i') ∘' α←' f' (g' ⊗' h') i' ∘' (f' ▶' α←' g' h' i'))
+          Hom[].≡[ pentagon f g h i ]
+          (α←' (f' ⊗' g') h' i' ∘' α←' f' g' (h' ⊗' i'))
+```
+
+## The displayed bicategory of displayed categories
+
+Displayed categories naturally assemble into a displayed biacategory over $\bf{Cat}$,
+with [[displayed functor categories|displayed-functor-category]] as $\hom$s.
+
+<!--
+```agda 
+open Bidisplayed hiding (_∘'_)
+```
+-->
+
+```agda
+Displayed-cat : ∀ o ℓ o' ℓ' → Bidisplayed (Cat o ℓ) _ _ _
+Displayed-cat o ℓ o' ℓ' .Ob[_] C = Displayed C o' ℓ'
+Displayed-cat o ℓ o' ℓ' .Hom[_,_] D E = Disp[ D , E ]
+Displayed-cat o ℓ o' ℓ' .↦id' = Id'
+Displayed-cat o ℓ o' ℓ' .compose' = F∘'-functor
+Displayed-cat o ℓ o' ℓ' .unitor-l' {B' = B'} = to-natural-iso' ni where
+  open DR B'
+  ni : make-natural-iso[ _ ] _ _
+  ni .eta' x' = NT' (λ _ → id') λ _ _ _ → id-comm-sym[]
+  ni .inv' x' = NT' (λ _ → id') λ _ _ _ → id-comm-sym[]
+  ni .eta∘inv' x' = Nat'-path λ x'' → idl' _
+  ni .inv∘eta' x' = Nat'-path λ x'' → idl' _
+  ni .natural' x' y' f' = Nat'-path λ x'' → cast[] $ symP $ (idr' _ ∙[] id-comm[])
+
+Displayed-cat o ℓ o' ℓ' .unitor-r' {B' = B'} = to-natural-iso' ni where
+  open DR B'
+  ni : make-natural-iso[ _ ] _ _
+  ni .eta' x' = NT' (λ _ → id') λ _ _ _ → id-comm-sym[]
+  ni .inv' x' = NT' (λ _ → id') λ _ _ _ → id-comm-sym[]
+  ni .eta∘inv' x' = Nat'-path λ x'' → idl' _
+  ni .inv∘eta' x' = Nat'-path λ x'' → idl' _
+  ni .natural' x' y' f' = Nat'-path λ x'' → cast[] $ (idl' _ ∙[] symP (idr' _ ∙[] ((y' .F-id' ⟩∘'⟨refl) ∙[] idl' _)))
+  
+Displayed-cat o ℓ o' ℓ' .associator' {C' = C'} {D' = D'} = to-natural-iso' ni where
+  open DR D'
+  module C' = Displayed C'
+  ni : make-natural-iso[ _ ] _ _ 
+  ni .eta' x' = NT' (λ _ → id') λ _ _ _ → id-comm-sym[]
+  ni .inv' x' = NT' (λ _ → id') λ _ _ _ → id-comm-sym[]
+  ni .eta∘inv' x' = Nat'-path (λ _ → idl' _)
+  ni .inv∘eta' x' = Nat'-path (λ _ → idl' _)
+  ni .natural' (x₁ , x₂ , x₃) (y₁ , y₂ , y₃) (α₁ , α₂ , α₃) = Nat'-path λ z → cast[] $
+    (idl' _ ∙[] symP (pushl[] _ (y₁ .F-∘')) ∙[] symP (idr' _))
+
+Displayed-cat o ℓ o' ℓ' .triangle' {B' = B'} {C' = C'} f' g' = Nat'-path λ x' → C'.idr' _ where
+  module C' = Displayed C'
+Displayed-cat o ℓ o' ℓ' .pentagon' {B' = B'} {C' = C'} {D' = D'} {E' = E'} f' g' h' i' = Nat'-path λ x' → cast[] $
+  (f' .F₁' (g' .F₁' (h' .F₁' B'.id')) ∘' id') ∘' (id' ∘' f' .F₁' D'.id' ∘' id') ≡[]⟨ idr' _ ⟩∘'⟨ idl' _ ⟩
+  (f' .F₁' (g' .F₁' (h' .F₁' B'.id'))) ∘' (f' .F₁' D'.id' ∘' id')               ≡[]⟨ ((apd (λ _ z → f' .F₁' (g' .F₁' z)) (h' .F-id')) ⟩∘'⟨ (idr' _)) ⟩ 
+  (f' .F₁' (g' .F₁' C'.id')) ∘' (f' .F₁' D'.id')                                ≡[]⟨ ((apd (λ _ → f' .F₁') (g' .F-id') ∙[] f' .F-id') ⟩∘'⟨ f' .F-id') ⟩
+  id' ∘' id'                                                                    ∎
+  where
+    open DR E'
+    module B' = Displayed B'
+    module C' = Displayed C'
+    module D' = Displayed D' 
+```
diff --git a/src/Cat/Bi/Instances/Displayed.lagda.md b/src/Cat/Bi/Instances/Displayed.lagda.md
index c01cdc887..2c4408a0d 100644
--- a/src/Cat/Bi/Instances/Displayed.lagda.md
+++ b/src/Cat/Bi/Instances/Displayed.lagda.md
@@ -106,8 +106,8 @@ as in the nondisplayed case.
       module D' {x} = Cat (Fibre D x) using (_∘_ ; idl ; idr ; elimr ; pushl ; introl)
 
       ni : make-natural-iso {D = Vf _ _} _ _
-      ni .eta _ = record { η' = λ x' → D.id' ; is-natural' = λ x y f → D.to-pathp[] D.id-comm[] }
-      ni .inv _ = record { η' = λ x' → D.id' ; is-natural' = λ x y f → D.to-pathp[] D.id-comm[] }
+      ni .eta _ = record { η' = λ x' → D.id' ; is-natural' = λ x y f → D.id-comm-sym[] }
+      ni .inv _ = record { η' = λ x' → D.id' ; is-natural' = λ x y f → D.id-comm-sym[] }
       ni .eta∘inv _ = ext λ _ → D'.idl _
       ni .inv∘eta _ = ext λ _ → D'.idl _
       ni .natural x y f = ext λ _ → D'.idr _ ∙∙ D'.pushl (F-∘↓ (y .fst)) ∙∙ D'.introl refl
@@ -127,8 +127,8 @@ the structural isomorphisms being identities.
   Disp[] .unitor-l {B = B} = to-natural-iso ni where
     module B = Disp B
     ni : make-natural-iso {D = Vf _ _} _ _
-    ni .eta _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → B.to-pathp[] B.id-comm[] }
-    ni .inv _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → B.to-pathp[] B.id-comm[] }
+    ni .eta _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → B.id-comm-sym[] }
+    ni .inv _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → B.id-comm-sym[] }
     ni .eta∘inv _ = ext λ _ → Cat.idl (Fibre B _) _
     ni .inv∘eta _ = ext λ _ → Cat.idl (Fibre B _) _
     ni .natural x y f = ext λ _ → Cat.elimr (Fibre B _) refl ∙ Cat.id-comm (Fibre B _)
@@ -137,8 +137,8 @@ the structural isomorphisms being identities.
     module B' {x} = Cat (Fibre B x) using (_∘_ ; idl ; elimr)
 
     ni : make-natural-iso {D = Vf _ _} _ _
-    ni .eta _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → B.to-pathp[] B.id-comm[] }
-    ni .inv _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → B.to-pathp[] B.id-comm[] }
+    ni .eta _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → B.id-comm-sym[] }
+    ni .inv _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → B.id-comm-sym[] }
     ni .eta∘inv _ = ext λ _ → B'.idl _
     ni .inv∘eta _ = ext λ _ → B'.idl _
     ni .natural x y f = ext λ _ → B'.elimr refl ∙ ap₂ B'._∘_ (y .F-id') refl
diff --git a/src/Cat/Displayed/Functor.lagda.md b/src/Cat/Displayed/Functor.lagda.md
index f547847bf..94eff4eac 100644
--- a/src/Cat/Displayed/Functor.lagda.md
+++ b/src/Cat/Displayed/Functor.lagda.md
@@ -123,8 +123,26 @@ module
     → (q1 : ∀ {x y x' y'} {f : A.Hom x y} → (f' : ℰ.Hom[ f ] x' y')
             → PathP (λ i → ℱ.Hom[ p i .F₁ f ] (q0 x' i) (q0 y' i)) (F' .F₁' f') (G' .F₁' f'))
     → PathP (λ i → Displayed-functor (p i) ℰ ℱ) F' G'
-  Displayed-functor-pathp {F = F} {G = G} {F' = F'} {G' = G'} p q0 q1 =
-    injectiveP (λ _ → eqv) ((λ i x' → q0 x' i) ,ₚ (λ i f' → q1 f' i) ,ₚ prop!)
+  Displayed-functor-pathp {F = F} {F' = F'} {G' = G'} p q0 q1 = dfn where
+    -- We need to define this directly to get nice definitional behavior on the projections
+    dfn : PathP (λ i → Displayed-functor (p i) ℰ ℱ) F' G'
+    dfn i .F₀' x' = q0 x' i
+    dfn i .F₁' f' = q1 f' i
+    dfn i .F-id' {x' = x'} j = 
+      is-set→squarep (λ i j → ℱ.Hom[ F-id (p i) j ]-set (q0 x' i) (q0 x' i)) 
+        (q1 ℰ.id') (F-id' F') (F-id' G') (λ _ → ℱ.id') i j
+    dfn i .F-∘' {f = f} {g = g} {a' = a'} {c' = c'} {f' = f'} {g' = g'} j = 
+      is-set→squarep (λ i j → ℱ.Hom[ F-∘ (p i) f g j ]-set (q0 a' i) (q0 c' i))
+        (q1 (f' ℰ.∘' g')) (F-∘' F') (F-∘' G') (λ k → q1 f' k ℱ.∘' q1 g' k) i j
+
+  Displayed-functor-is-set : {F : Functor A B} → (∀ x → is-set ℱ.Ob[ x ]) → is-set (Displayed-functor F ℰ ℱ)
+  Displayed-functor-is-set fibre-set = Iso→is-hlevel! 2 eqv where instance
+    ℱOb[] : ∀ {x} → H-Level (ℱ.Ob[ x ]) 2
+    ℱOb[] = hlevel-instance (fibre-set _)
+
+  instance
+    Funlike-displayed-functor : ∀ {F : Functor A B} {x} → Funlike (Displayed-functor F ℰ ℱ) (⌞ ℰ.Ob[ x ] ⌟) λ _ → ⌞ ℱ.Ob[ F .F₀ x ] ⌟
+    Funlike-displayed-functor = record { _·_ = λ F x → F .F₀' x }
 ```
 -->
 
@@ -395,6 +413,9 @@ module
             → PathP (λ i → ℱ.Hom[ f ] (p0 x' i) (p0 y' i)) (F .F₁' f') (G .F₁' f'))
     → F ≡ G
   Vertical-functor-path = Displayed-functor-pathp refl
+
+  Vertical-functor-is-set : (∀ x → is-set ℱ.Ob[ x ]) → is-set (Vertical-functor ℰ ℱ)
+  Vertical-functor-is-set fibre-set = Displayed-functor-is-set fibre-set
 ```
 -->
 
@@ -458,6 +479,7 @@ module
     (G' : Displayed-functor G ℰ ℱ)
     : Type lvl
     where
+    constructor NT'
     no-eta-equality
 
     field
@@ -467,6 +489,82 @@ module
         → η' y' ℱ.∘' F' .F₁' f' ℱ.≡[ α .is-natural x y f ] G' .F₁' f' ℱ.∘' η' x'
 ```
 
+<!--
+```agda
+{-# INLINE NT' #-}
+
+unquoteDecl H-Level-=[]=> = declare-record-hlevel 2 H-Level-=[]=> (quote _=[_]=>_)
+
+module _
+  {oa ℓa ob ℓb od ℓd oe ℓe}
+  {A : Precategory oa ℓa} {B : Precategory ob ℓb}
+  {D : Displayed A od ℓd} {E : Displayed B oe ℓe}
+  where
+  private 
+    module A = Precategory A
+    module B = Precategory B
+    module D = Displayed D
+    module E = DR E
+
+  open _=>_
+  open _=[_]=>_
+  open Displayed-functor
+
+  Nat'-pathp : {F₁ F₂ G₁ G₂ : Functor A B} 
+             → {F₁' : Displayed-functor F₁ D E} 
+             → {G₁' : Displayed-functor G₁ D E}
+             → {F₂' : Displayed-functor F₂ D E}
+             → {G₂' : Displayed-functor G₂ D E}
+             → {α : F₁ => G₁} {β : F₂ => G₂}
+             → {α' : F₁' =[ α ]=> G₁'} {β' : F₂' =[ β ]=> G₂'}
+             → (p : F₁ ≡ F₂) (q : G₁ ≡ G₂) 
+             → (r : PathP (λ i → p i => q i) α β)
+             → (p' : PathP (λ i → Displayed-functor (p i) D E) F₁' F₂')
+             → (q' : PathP (λ i → Displayed-functor (q i) D E) G₁' G₂')
+             → (∀ {x} (x' : D.Ob[ x ]) → PathP (λ i → E.Hom[ (r i .η x) ] (p' i .F₀' x') (q' i .F₀' x')) (α' .η' x') (β' .η' x'))
+             → PathP (λ i → (p' i) =[ r i ]=> (q' i)) α' β'
+  Nat'-pathp p q r p' q' w i .η' x' = w x' i
+  Nat'-pathp {α' = α'} {β' = β'} p q r p' q' w i .is-natural' {x = x} {y} {f} x' y' f' j = 
+    is-set→squarep {A = λ i j → E.Hom[ r i .is-natural x y f j ] (F₀' (p' i) x') (F₀' (q' i) y')} (λ _ _ → hlevel 2)
+      (λ i → w y' i E.∘' F₁' (p' i) f') (λ j → is-natural' α' x' y' f' j) (λ j → is-natural' β' x' y' f' j) (λ i → F₁' (q' i) f' E.∘' w x' i) i j
+
+  Nat'-path : {F G : Functor A B} {F' : Displayed-functor F D E} {G' : Displayed-functor G D E}
+           → {α β : F => G} {α' : F' =[ α ]=> G'} {β' : F' =[ β ]=> G'} 
+           → {p : α ≡ β}
+           → (∀ {x} (x' : D.Ob[ x ]) → α' .η' x' E.≡[ p ηₚ x ] β' .η' x')
+           → PathP (λ i → F' =[ p i ]=> G') α' β'
+  Nat'-path = Nat'-pathp refl refl _ refl refl
+```
+-->
+
+We can define displayed versions of the identity natural transformation and 
+composition of natural transformations.
+
+```agda 
+  idnt' : ∀ {F : Functor A B} {F' : Displayed-functor F D E} → F' =[ idnt ]=> F'
+  idnt' .η' x' = E.id'
+  idnt' .is-natural' x' y' f' = E.id-comm-sym[]
+
+  _∘nt'_ : ∀ {F G H : Functor A B} 
+          → {F' : Displayed-functor F D E} 
+          → {G' : Displayed-functor G D E} 
+          → {H' : Displayed-functor H D E} 
+          → {β : G => H} {α : F => G}
+          → G' =[ β ]=> H' → F' =[ α ]=> G' → F' =[ β ∘nt α ]=> H'
+  (β' ∘nt' α') .η' x' = β' .η' x' E.∘' α' .η' x'
+  _∘nt'_ {F' = F'} {G'} {H'} β' α' .is-natural' x' y' f' = E.cast[] $ 
+    (β'.η' y' E.∘' α'.η' y') E.∘' F'.F₁' f'  E.≡[]⟨ E.pullr[] _ (α'.is-natural' _ _ _) ⟩
+      β'.η' y' E.∘' G'.F₁' f' E.∘' α'.η' x'  E.≡[]⟨ E.pulll[] _ (β'.is-natural' _ _ _) ⟩
+    (H'.F₁' f' E.∘' β'.η' x') E.∘' α'.η' x'  E.≡[]˘⟨ E.assoc' _ _ _ ⟩
+      H'.F₁' f' E.∘' β'.η' x' E.∘' α'.η' x'   ∎
+    where
+      module β' = _=[_]=>_ β'
+      module α' = _=[_]=>_ α'
+      module F' = Displayed-functor F'
+      module G' = Displayed-functor G'
+      module H' = Displayed-functor H'
+```
+
 ::: {.definition #vertical-natural-transformation}
 Let $F, G : \cE \to \cF$ be two vertical functors. A displayed natural
 transformation between $F$ and $G$ is called a **vertical natural
@@ -522,14 +620,11 @@ module _
     Extensional-=>↓ {F' = F'} {G' = G'}  ⦃ e ⦄  = injection→extensional! {f = _=>↓_.η'}
       (λ p → Iso.injective eqv (Σ-prop-path! p)) e
 
-    H-Level-=>↓ : ∀ {F' G'} {n} → H-Level (F' =>↓ G') (2 + n)
-    H-Level-=>↓ = basic-instance 2 (Iso→is-hlevel 2 eqv (hlevel 2))
-
   open _=>↓_
 
   idnt↓ : ∀ {F} → F =>↓ F
   idnt↓ .η' x' = ℱ.id'
-  idnt↓ .is-natural' x' y' f' = ℱ.to-pathp[] (DR.id-comm[] ℱ)
+  idnt↓ .is-natural' x' y' f' = DR.id-comm-sym[] ℱ
 
   _∘nt↓_ : ∀ {F G H} → G =>↓ H → F =>↓ G → F =>↓ H
   (f ∘nt↓ g) .η' x' = f .η' _ ℱ↓.∘ g .η' x'
diff --git a/src/Cat/Displayed/Functor/Naturality.lagda.md b/src/Cat/Displayed/Functor/Naturality.lagda.md
new file mode 100644
index 000000000..ffc12dc97
--- /dev/null
+++ b/src/Cat/Displayed/Functor/Naturality.lagda.md
@@ -0,0 +1,103 @@
+<!--
+```agda
+open import Cat.Displayed.Instances.DisplayedFunctor
+open import Cat.Functor.Naturality
+open import Cat.Displayed.Functor
+open import Cat.Displayed.Base
+open import Cat.Morphism
+open import Cat.Prelude
+
+import Cat.Displayed.Reasoning as DR
+import Cat.Displayed.Morphism as DM
+```
+-->
+
+```agda
+module Cat.Displayed.Functor.Naturality where
+```
+
+# Natural isomorhisms of displayed functors
+
+We define displayed versions of our functor naturality tech.
+
+<!--
+```agda
+module _ 
+  {ob ℓb oc ℓc od ℓd oe ℓe} 
+  {B : Precategory ob ℓb} {C : Precategory oc ℓc}
+  {D : Displayed B od ℓd} {E : Displayed C oe ℓe}
+  where
+  private
+    module B = Precategory B
+    module C = Precategory C
+    module DE where
+      open DR Disp[ D , E ] public 
+      open DM Disp[ D , E ] public
+    module D = DR D
+    module E = DR E
+    
+  open Functor
+  open _=>_
+  open Displayed-functor
+  open _=[_]=>_
+```
+-->
+
+```agda
+
+  _≅[_]ⁿ_ : {F G : Functor B C} → Displayed-functor F D E → F ≅ⁿ G → Displayed-functor G D E → Type _
+  F ≅[ i ]ⁿ G = F DE.≅[ i ] G
+
+
+  is-natural-transformation' 
+    : {F G : Functor B C} (F' : Displayed-functor F D E) (G' : Displayed-functor G D E)
+    → (α : F => G)
+    → (η' : ∀ {x} (x' : D.Ob[ x ]) → E.Hom[ α .η x ] (F' .F₀' x') (G' .F₀' x'))
+    → Type _
+  is-natural-transformation' F' G' α η' = 
+    ∀ {x y f} (x' : D.Ob[ x ]) (y' : D.Ob[ y ]) (f' : D.Hom[ f ] x' y')
+        → η' y' E.∘' F' .F₁' f' E.≡[ α .is-natural x y f ] G' .F₁' f' E.∘' η' x'
+
+  inverse-is-natural'
+    : ∀ {F G : Functor B C} (iso : F ≅ⁿ G) {F' : Displayed-functor F D E} {G' : Displayed-functor G D E}
+    → (α' : F' =[ iso .to ]=> G')
+    → (β' : ∀ {x} (x' : D.Ob[ x ]) → E.Hom[ iso .from .η x ] (G' .F₀' x') (F' .F₀' x'))
+    → (∀ {x} (x' : D.Ob[ x ]) → α' .η' x' E.∘' β' x' E.≡[ iso .invl ηₚ x ] E.id')
+    → (∀ {x} (x' : D.Ob[ x ]) → β' x' E.∘' α' .η' x' E.≡[ iso .invr ηₚ x ] E.id')
+    → is-natural-transformation' G' F' (iso .from) β'
+  inverse-is-natural' i {F'} {G'} α' β' invl' invr' x' y' f' = E.cast[] $ 
+    β' y' E.∘' G' .F₁' f'                           E.≡[]⟨ E.refl⟩∘'⟨ E.intror[] _ (invl' x') ⟩ 
+    β' y' E.∘' G' .F₁' f' E.∘' α' .η' x' E.∘' β' x' E.≡[]⟨ E.refl⟩∘'⟨ E.extendl[] _ (symP (α' .is-natural' _ _ _)) ⟩
+    β' y' E.∘' α' .η' y' E.∘' F' .F₁' f' E.∘' β' x' E.≡[]⟨ E.cancell[] _ (invr' _) ⟩
+    F' .F₁' f' E.∘' β' x'                           ∎
+
+
+  record make-natural-iso[_] {F G : Functor B C} (iso : F ≅ⁿ G) (F' : Displayed-functor F D E) (G' : Displayed-functor G D E) : Type (ob ⊔ ℓb ⊔ od ⊔ ℓd ⊔ ℓe) where
+    no-eta-equality
+    field
+      eta' : ∀ {x} (x' : D.Ob[ x ]) → E.Hom[ iso .to .η x   ] (F' .F₀' x') (G' .F₀' x')
+      inv' : ∀ {x} (x' : D.Ob[ x ]) → E.Hom[ iso .from .η x ] (G' .F₀' x') (F' .F₀' x')
+      eta∘inv' : ∀ {x} (x' : D.Ob[ x ]) → eta' x' E.∘' inv' x' E.≡[ (λ i → iso .invl i .η x) ] E.id'
+      inv∘eta' : ∀ {x} (x' : D.Ob[ x ]) → inv' x' E.∘' eta' x' E.≡[ (λ i → iso .invr i .η x) ] E.id'
+      natural' : ∀ {x y} x' y' {f : B.Hom x y} (f' : D.Hom[ f ] x' y')
+               →  eta' y' E.∘' F' .F₁' f' E.≡[ (λ i → iso .to .is-natural x y f i) ]  G' .F₁' f' E.∘' eta' x'
+
+
+  open make-natural-iso[_]
+
+  to-natural-iso' : {F G : Functor B C} {iso : F ≅ⁿ G} {F' : Displayed-functor F D E} {G' : Displayed-functor G D E}
+                  → make-natural-iso[ iso ] F' G' → F' ≅[ iso ]ⁿ G'
+  to-natural-iso' {iso = i} mk = 
+    let to' = record { η' = mk .eta' ; is-natural' = λ {x} {y} {f} x' y' → mk .natural' x' y' } in
+    record 
+      { to' = to'
+      ; from' = record { η' = mk .inv' ; is-natural' = inverse-is-natural' i to' (mk .inv') (mk .eta∘inv') (mk .inv∘eta') } 
+      ; inverses' = record { invl' = Nat'-path (mk .eta∘inv') ; invr' = Nat'-path (mk .inv∘eta') } 
+      }
+```
+
+<!--
+```agda
+  {-# INLINE to-natural-iso' #-}
+```
+-->
diff --git a/src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md b/src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md
new file mode 100644
index 000000000..af439ce25
--- /dev/null
+++ b/src/Cat/Displayed/Instances/DisplayedFunctor.lagda.md
@@ -0,0 +1,125 @@
+<!--
+```agda
+open import Cat.Displayed.Instances.TotalProduct
+open import Cat.Displayed.Functor
+open import Cat.Instances.Functor
+open import Cat.Functor.Compose
+open import Cat.Displayed.Base
+open import Cat.Reasoning as CR
+open import Cat.Prelude
+
+import Cat.Displayed.Reasoning as DR
+```
+-->
+
+```agda
+module Cat.Displayed.Instances.DisplayedFunctor where
+```
+
+# Displayed functor categories {defines=displayed-functor-category}
+
+Given two displayed categories $\cD \liesover \cA$ and $\cE \liesover \cB$, we
+can assemble them into a displayed category $[\cD, \cE] \liesover [\cA, \cB]$.
+The construction mirrors the construction of ordinary functor categories,
+using displayed versions of all the same data.
+
+<!--
+```agda
+open _=>_
+open _=[_]=>_
+open Functor
+open Displayed-functor
+
+module _ 
+  {oa ℓa ob ℓb oa' ℓa' ob' ℓb'} 
+  {A : Precategory oa ℓa} {B : Precategory ob ℓb}
+  (D : Displayed A oa' ℓa') (E : Displayed B ob' ℓb')
+  where
+  private
+    module A = CR A
+    module B = CR B
+    module D = Displayed D
+    module E = DR E
+```
+-->
+
+```agda
+  Disp[_,_] : Displayed (Cat[ A , B ]) _ _
+  Disp[_,_] .Displayed.Ob[_] f = Displayed-functor f D E
+  Disp[_,_] .Displayed.Hom[_] α F' G' = F' =[ α ]=> G'
+  Disp[_,_] .Displayed.Hom[_]-set _ _ _ = hlevel 2
+  Disp[_,_] .Displayed.id' = idnt'
+  Disp[_,_] .Displayed._∘'_ = _∘nt'_
+  Disp[_,_] .Displayed.idr' _ = Nat'-path λ x' → E.idr' _
+  Disp[_,_] .Displayed.idl' _ = Nat'-path λ x' → E.idl' _
+  Disp[_,_] .Displayed.assoc' _ _ _ = Nat'-path λ x' → E.assoc' _ _ _
+  Disp[_,_] .Displayed.hom[_] {x = F} {y = G} p α' = NT' (λ {x} x' → E.hom[ p ηₚ x ] (α' .η' x')) 
+    λ {x} {y} x' y' f' → E.cast[] $ E.unwrapl _ E.∙[] α' .is-natural' x' y' f' E.∙[] E.wrapr _
+  Disp[_,_] .Displayed.coh[_] p f = Nat'-path (λ {x} x' → E.coh[ p ηₚ x ] (f .η' x'))
+```
+
+<!--
+```agda
+module _ 
+  {oa ℓa ob ℓb oc ℓc oa' ℓa' ob' ℓb' oc' ℓc'} 
+  {A : Precategory oa ℓa} {B : Precategory ob ℓb}
+  {C : Precategory oc ℓc} 
+  {A' : Displayed A oa' ℓa'} {B' : Displayed B ob' ℓb'}
+  {C' : Displayed C oc' ℓc'} 
+  {F G : Functor B C} {H K : Functor A B}
+  {α : F => G} {β : H => K}
+  {F' : Displayed-functor F B' C'} {G' : Displayed-functor G B' C'}
+  {H' : Displayed-functor H A' B'} {K' : Displayed-functor K A' B'}
+  where
+  private
+    module B' = Displayed B'
+    module C' = DR C'
+```
+-->
+
+We can also construct a displayed version of the [[functor composition functor|composition-functor]]. 
+First we'll define displayed horizontal composition of natural transformations.
+
+```agda
+  _◆'_ : F' =[ α ]=> G' → H' =[ β ]=> K' → F' F∘' H' =[ α ◆ β ]=> G' F∘' K'
+  (α' ◆' β') .η' x' = G' .F₁' (β' .η' _) C'.∘' α' .η' _
+  (α' ◆' β') .is-natural' x' y' f' = cast[] $
+    (G' .F₁' (β' .η' y') ∘' α' .η' (H' .F₀' y')) ∘' F' .F₁' (H' .F₁' f')  ≡[]⟨ pullr[] _ (α' .is-natural' _ _ _) ⟩
+     G' .F₁' (β' .η' y') ∘' G' .F₁' (H' .F₁' f') ∘' α' .η' (H' .F₀' x')   ≡[]⟨ pulll[] _ (symP (G' .F-∘') ∙[] apd (λ _ → G' .F₁') (β' .is-natural' _ _ _) ∙[] G' .F-∘') ⟩
+    (G' .F₁' (K' .F₁' f') ∘' G' .F₁' (β' .η' x')) ∘' α' .η' (H' .F₀' x')  ≡[]˘⟨ assoc' _ _ _ ⟩ 
+     G' .F₁' (K' .F₁' f') ∘' G' .F₁' (β' .η' x') ∘' α' .η' (H' .F₀' x')   ∎  
+    where open C'
+```
+
+<!--
+```agda
+module _ 
+  {oa ℓa ob ℓb oc ℓc oa' ℓa' ob' ℓb' oc' ℓc'} 
+  {A : Precategory oa ℓa} {B : Precategory ob ℓb}
+  {C : Precategory oc ℓc} 
+  {A' : Displayed A oa' ℓa'} {B' : Displayed B ob' ℓb'}
+  {C' : Displayed C oc' ℓc'} 
+  where
+  private 
+    module C = Precategory C
+    module C' = Displayed C'
+```
+-->
+
+:::{.definition #displayed-composition-functor}
+Armed with this, we can define our displayed composition functor.
+:::
+
+```agda
+  F∘'-functor : Displayed-functor F∘-functor (Disp[ B' , C' ] ×ᵀᴰ Disp[ A' , B' ]) Disp[ A' , C' ]
+  F∘'-functor .F₀' (F' , G') = F' F∘' G' 
+  F∘'-functor .F₁' (α' , β') = α' ◆' β'
+  F∘'-functor .F-id' {F , G} {F' , G'} = 
+    Nat'-path λ x' → C'.idr' _ C'.∙[] F' .F-id'
+  F∘'-functor .F-∘' {a' = F' , G'} {H' , I'} {J' , K'} {α' , _} {β' , _} =
+    Nat'-path λ x' → 
+        pushl[] _ (J' .F-∘')                              C'.∙[] 
+        ((extend-inner' _ (symP (α' .is-natural' _ _ _))) C'.∙[] 
+        (pulll' refl refl))
+      where open DR C'
+```
diff --git a/src/Cat/Displayed/Instances/TotalProduct.lagda.md b/src/Cat/Displayed/Instances/TotalProduct.lagda.md
index b3157ba23..595899d3c 100644
--- a/src/Cat/Displayed/Instances/TotalProduct.lagda.md
+++ b/src/Cat/Displayed/Instances/TotalProduct.lagda.md
@@ -5,24 +5,28 @@ open import 1Lab.HLevel.Closure
 open import 1Lab.Type.Sigma
 
 open import Cat.Instances.Sets.Complete
+open import Cat.Displayed.Functor
 open import Cat.Instances.Product
 open import Cat.Diagram.Product
 open import Cat.Displayed.Base
 open import Cat.Instances.Sets
 open import Cat.Prelude
 open import Cat.Base
+
+import Cat.Displayed.Reasoning as DR
+import Cat.Functor.Bifunctor
 ```
 -->
 
 ```agda
-module Cat.Displayed.Instances.TotalProduct
+module Cat.Displayed.Instances.TotalProduct where
 ```
-
 <!--
 ```agda
+module _ 
   {o₁ ℓ₁ o₂ ℓ₂ o₃ ℓ₃ o₄ ℓ₄}
-  (C : Precategory o₁ ℓ₁)
-  (D : Precategory o₂ ℓ₂)
+  {C : Precategory o₁ ℓ₁}
+  {D : Precategory o₂ ℓ₂}
   (EC : Displayed C o₃ ℓ₃) (ED : Displayed D o₄ ℓ₄) where
   private module EC = Displayed EC
   private module ED = Displayed ED
@@ -37,6 +41,7 @@ $\cE\times \cD\to \cB\times \cC$,
 which is again a displayed category.
 
 ```agda
+  infixr 20 _×ᵀᴰ_
   _×ᵀᴰ_ : Displayed (C ×ᶜ D) (o₃ ⊔ o₄) (ℓ₃ ⊔ ℓ₄)
 ```
 
@@ -78,9 +83,75 @@ they hold for the components of the ordered pairs.
   _×ᵀᴰ_ .Displayed.idl' (f₁ , f₂) = EC.idl' f₁ ,ₚ ED.idl' f₂
   _×ᵀᴰ_ .Displayed.assoc' (f₁ , f₂) (g₁ , g₂) (h₁ , h₂) =
     EC.assoc' f₁ g₁ h₁ ,ₚ ED.assoc' f₂ g₂ h₂
-```
 
-```agda
   _×ᵀᴰ_ .Displayed.hom[_] p f = EC.hom[ ap fst p ] (f .fst) ,  ED.hom[ ap snd p ] (f .snd)
   _×ᵀᴰ_ .Displayed.coh[_] p f = EC.coh[ ap fst p ] (f .fst) ,ₚ ED.coh[ ap snd p ] (f .snd)
 ```
+
+<!--
+```agda
+module _
+  {oa ℓa ob ℓb oc ℓc oa' ℓa' ob' ℓb' oc' ℓc'}
+  {A : Precategory oa ℓa} {B : Precategory ob ℓb} {C : Precategory oc ℓc}
+  {A' : Displayed A oa' ℓa'} {B' : Displayed B ob' ℓb'} {C' : Displayed C oc' ℓc'}
+  {F : Functor (A ×ᶜ B) C}
+  (F' : Displayed-functor F (A' ×ᵀᴰ B') C')
+  where
+  private
+    module A = Precategory A
+    module B = Precategory B
+    module C = Precategory C
+    module A' = DR A'
+    module B' = DR B'
+    module C' = DR C'
+  
+  open Displayed-functor F'
+  open Cat.Functor.Bifunctor F
+```
+-->
+
+Using the total product we can define displayed versions of these familiar bifunctor constructions.
+
+```agda
+  first' : ∀ {a b a' b'} {f : A.Hom a b} {x} {x' : B'.Ob[ x ]} → A'.Hom[ f ] a' b' → C'.Hom[ first f ] (F₀' (a' , x')) (F₀' (b' , x'))
+  first' f' = F₁' (f' , B'.id')
+
+  second' : ∀ {a b a' b'} {f : B.Hom a b} {x} {x' : A'.Ob[ x ]} → B'.Hom[ f ] a' b' → C'.Hom[ second f ] (F₀' (x' , a')) (F₀' (x' , b'))
+  second' f' = F₁' (A'.id' , f')
+
+  first-id' : ∀ {a x} {a' : B'.Ob[ a ]} {x' : A'.Ob[ x ]} → first' A'.id' C'.≡[ first-id ] C'.id' {x = F₀' (x' , a')}
+  first-id' = F-id'
+
+  second-id' : ∀ {a x} {a' : A'.Ob[ a ]} {x' : B'.Ob[ x ]} → second' B'.id' C'.≡[ second-id ] C'.id' {x = F₀' (a' , x')}
+  second-id' = F-id'
+
+  first∘first' : ∀ {a b c a' b' c'} {x x'} {f : A.Hom b c} {g : A.Hom a b}
+               → {f' : A'.Hom[ f ] b' c'} {g' : A'.Hom[ g ] a' b'}
+               → first' {x = x} {x'} (f' A'.∘' g') C'.≡[ first∘first ] first' f' C'.∘' first' g'
+  first∘first' {f' = f'} {g' = g'} = C'.cast[] $ symP $
+    F₁' (f' , B'.id') C'.∘' F₁' (g' , B'.id') C'.≡[]⟨ symP F-∘' ⟩ 
+    F₁' (f' A'.∘' g' , B'.id' B'.∘' B'.id')   C'.≡[]⟨ apd (λ _ e → F₁' (f' A'.∘' g' , e)) (B'.idl' _) ⟩
+    F₁' (f' A'.∘' g' , B'.id')                ∎
+
+  second∘second' : ∀ {a b c a' b' c'} {x x'} {f : B.Hom b c} {g : B.Hom a b}
+                  → {f' : B'.Hom[ f ] b' c'} {g' : B'.Hom[ g ] a' b'}
+                  → second' {x = x} {x'} (f' B'.∘' g')
+                  C'.≡[ second∘second ]
+                    second' f' C'.∘' second' g'
+  second∘second' {f' = f'} {g' = g'} = C'.cast[] $ symP $
+    F₁' (A'.id' , f') C'.∘' F₁' (A'.id' , g') C'.≡[]⟨ symP F-∘' ⟩
+    F₁' (A'.id' A'.∘' A'.id' , f' B'.∘' g')   C'.≡[]⟨ apd (λ _ e → F₁' (e , f' B'.∘' g')) (A'.idl' _) ⟩
+    F₁' (A'.id' , f' B'.∘' g')                ∎
+
+  Left' : ∀ {y} → B'.Ob[ y ] → Displayed-functor (Left y) A' C'
+  Left' y' .F₀' x' = F₀' (x' , y')
+  Left' y' .F₁' = first'
+  Left' y' .F-id' = F-id'
+  Left' y' .F-∘' = first∘first'
+
+  Right' : ∀ {x} → A'.Ob[ x ] → Displayed-functor (Right x) B' C'
+  Right' x .F₀' y' = F₀' (x , y')
+  Right' x .F₁' = second'
+  Right' x .F-id' = F-id'
+  Right' x .F-∘' = second∘second'
+```
diff --git a/src/Cat/Displayed/Reasoning.lagda.md b/src/Cat/Displayed/Reasoning.lagda.md
index cb44ad395..fbf811ef2 100644
--- a/src/Cat/Displayed/Reasoning.lagda.md
+++ b/src/Cat/Displayed/Reasoning.lagda.md
@@ -454,8 +454,23 @@ module _ {f' : Hom[ f ] x' y'} where abstract
   idr[] : {p : f ∘ id ≡ f} → hom[ p ] (f' ∘' id') ≡ f'
   idr[] {p = p} = reindex p (idr _) ∙ from-pathp[] (idr' f')
 
-  id-comm[] : {p : id ∘ f ≡ f ∘ id} → hom[ p ] (id' ∘' f') ≡ f' ∘' id'
-  id-comm[] {p = p} = duplicate _ _ _ ∙ ap hom[] (from-pathp[] (idl' _)) ∙ from-pathp[] (symP (idr' _))
+  id-comm' : {p : f ∘ id ≡ id ∘ f} → (f' ∘' id') ≡[ p ] id' ∘' f'
+  id-comm' = cast[] (idr' _ ∙[] symP (idl' _))
+
+  id-comm[] : (f' ∘' id') ≡[ id-comm ] id' ∘' f'
+  id-comm[] = id-comm'
+
+  id-comm-sym' : {p : id ∘ f ≡ f ∘ id} → (id' ∘' f') ≡[ p ] f' ∘' id'
+  id-comm-sym' = cast[] (idl' _ ∙[] symP (idr' _))
+
+  id-comm-sym[] : (id' ∘' f') ≡[ id-comm-sym ] f' ∘' id'
+  id-comm-sym[] = id-comm-sym'
+
+  id2' : ∀ {a} {x : Ob[ a ]} {p : id ∘ id ≡ id} → id' {x = x} ∘' id' ≡[ p ] id'
+  id2' = cast[] (idl' id')
+
+  id2[] : ∀ {a} {x : Ob[ a ]} → id' {x = x} ∘' id' ≡[ id2 ] id'
+  id2[] = id2'
 
 assoc[]
   : ∀ {a' : Hom[ a ] y' z'} {b' : Hom[ b ] x' y'} {c' : Hom[ c ] w' x'}
diff --git a/src/Cat/Displayed/Section.lagda.md b/src/Cat/Displayed/Section.lagda.md
index ed27204ba..fcb7ac878 100644
--- a/src/Cat/Displayed/Section.lagda.md
+++ b/src/Cat/Displayed/Section.lagda.md
@@ -133,7 +133,7 @@ module _ {o ℓ o' ℓ'} {B : Precategory o ℓ} (E : Displayed B o' ℓ') where
   Sections .Ob          = Section E
   Sections .Hom         = _=>s_
   Sections .Hom-set X Y = hlevel 2
-  Sections .id      = record { map = λ x → id' ; com = λ x y f → to-pathp[] id-comm[] }
+  Sections .id      = record { map = λ x → id' ; com = λ x y f → id-comm-sym[] }
   Sections ._∘_ {S} {T} {U} f g = record
     { map = λ x     → hom[ B.idl B.id ] (f .map x ∘' g .map x)
     ; com = λ x y h → cast[] $
diff --git a/src/Cat/Functor/Compose.lagda.md b/src/Cat/Functor/Compose.lagda.md
index 08e8909ad..bdfdc1071 100644
--- a/src/Cat/Functor/Compose.lagda.md
+++ b/src/Cat/Functor/Compose.lagda.md
@@ -90,7 +90,9 @@ _◆_ {E = E} {F = F} {G} {H} {K} α β = nat module horizontal-comp where
 ```
 -->
 
+:::{.definition #composition-functor}
 We can now define the composition functor itself.
+:::
 
 ```agda
 F∘-functor : Functor (Cat[ B , C ] ×ᶜ Cat[ A , B ]) Cat[ A , C ]
diff --git a/src/bibliography.bibtex b/src/bibliography.bibtex
index 14155e0af..f29e804e5 100644
--- a/src/bibliography.bibtex
+++ b/src/bibliography.bibtex
@@ -340,3 +340,16 @@
   pages      = {153–192},
   numpages   = {40}
   }
+
+@article{Ahrens-Frumin-Maggesi-Veltre-vanDerWeide:Bicategories,
+  title = {Bicategories in univalent foundations},
+  author = {Ahrens B, Frumin D, Maggesi M, Veltri N, van der Weide N},
+  year = {2022},
+  publisher = {Cambridge University Press},
+  journal   = {Mathematical Structures in Computer Science},
+  volume = {31},
+  number = {10},
+  pages = {1232-1269},
+  doi = {10.1017/S0960129522000032},
+  url = {https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science/article/bicategories-in-univalent-foundations/8BFCD0A0A5DD385C130DB28BCD5E3F68}
+}