diff --git a/src/Cat/Displayed/Bifibration.lagda.md b/src/Cat/Displayed/Bifibration.lagda.md
new file mode 100644
index 000000000..c220095ed
--- /dev/null
+++ b/src/Cat/Displayed/Bifibration.lagda.md
@@ -0,0 +1,132 @@
+```agda
+open import Cat.Displayed.Base
+open import Cat.Displayed.Fibre
+open import Cat.Functor.Adjoint
+open import Cat.Functor.Adjoint.Hom
+open import Cat.Instances.Functor
+open import Cat.Prelude
+
+import Cat.Displayed.Cartesian.Indexing
+import Cat.Displayed.Cocartesian.Indexing
+import Cat.Displayed.Cocartesian
+import Cat.Displayed.Cocartesian.Weak
+import Cat.Displayed.Cartesian
+import Cat.Displayed.Cartesian.Weak
+import Cat.Displayed.Reasoning
+import Cat.Reasoning
+
+module Cat.Displayed.Bifibration
+  {o ℓ o′ ℓ′} {ℬ : Precategory o ℓ} (ℰ : Displayed ℬ o′ ℓ′) where
+```
+
+<!--
+```agda
+open Cat.Displayed.Cocartesian ℰ
+open Cat.Displayed.Cocartesian.Weak ℰ
+open Cat.Displayed.Cartesian ℰ
+open Cat.Displayed.Cartesian.Weak ℰ
+open Cat.Displayed.Reasoning ℰ
+
+open Precategory ℬ
+open Displayed ℰ
+```
+-->
+
+
+# Bifibrations
+
+A displayed category $\cE \liesover \cB$ is a **bifibration** if it both
+a fibration and an opfibration. This means that $\cE$ is equipped with
+both [reindexing] and [opreindexing] functors, which allows us to both
+restrict and extend along morphisms $X \to Y$ in the base.
+
+Note that a bifibration is *not* the same as a "profunctor of categories";
+these are called **two-sided fibrations**, and are a distinct concept.
+
+[reindexing]: Cat.Displayed.Cartesian.Indexing.html
+[opreindexing]: Cat.Displayed.Cocartesian.Indexing.html
+
+<!--
+[TODO: Reed M, 31/01/2023] Link to two-sided fibration
+when that page is written.
+-->
+
+
+```agda
+record is-bifibration : Type (o ⊔ ℓ ⊔ o′ ⊔ ℓ′) where
+  field
+    fibration : Cartesian-fibration
+    opfibration : Cocartesian-fibration
+
+  module fibration = Cartesian-fibration fibration
+  module opfibration = Cocartesian-fibration opfibration
+```
+
+# Bifibrations and Adjoints
+
+If $\cE$ is a bifibration, then its opreindexing functors are
+[left adjoints] to reindexing functors. To see this, note that we need
+to construct a natural isomorphism between $\cE_{y}(u_{*}(-),-)$ and
+$\cE_{x}(-,u^{*}(-))$. However, we have already shown that
+$\cE_{y}(u_{*}(-),-)$ and $\cE_{x}(-,u^{*}(-))$ are both naturally
+isomorphic to $\cE_{u}(-,-)$ (see `opfibration→hom-iso`{.Agda} and
+`fibration→hom-iso`{.Agda}), so all we need to do is compose these
+natural isomorphisms!
+
+[left adjoints]: Cat.Functor.Adjoint.html
+
+```agda
+module _ (bifib : is-bifibration) where
+  open is-bifibration bifib
+  open Cat.Displayed.Cartesian.Indexing ℰ fibration
+  open Cat.Displayed.Cocartesian.Indexing ℰ opfibration
+
+  cobase-change⊣base-change
+    : ∀ {x y} (f : Hom x y)
+    → cobase-change f ⊣ base-change f
+  cobase-change⊣base-change {x} {y} f =
+    hom-natural-iso→adjoints $
+      (opfibration→hom-iso opfibration f ni⁻¹) ni∘ fibration→hom-iso fibration f
+```
+
+In fact, if $\cE$ is a cartesian fibration where every reindexing
+functor has a left adjoint, then $\cE$ is a bifibration!
+To see this, note that we have a natural iso
+$\cE_{u}(x',-) \simeq \cE_{x}(x', u^{*}(-))$ for every $u : x \to y$ in
+the base. However, $u^{*}$ has a left adjoint $L_{u}$ for every $u$,
+so we also have a natural isomorphism
+$\cE_{x}(x', u^{*}(-)) \simeq \cE_{y}(L_{u}(x'),-)$. Composing these
+yields a natural iso $\cE_{u}(x',-) \simeq \cE_{y}(L_{u}(x'),-)$, which
+implies that $\cE$ is a weak opfibration due to
+`hom-iso→weak-opfibration`{.Agda}.
+
+Furthermore, $\cE$ is a fibration, which allows us to upgrade the
+weak opfibration to an opfibration!
+
+```agda
+module _ (fib : Cartesian-fibration) where
+  open Cartesian-fibration fib
+  open Cat.Displayed.Cartesian.Indexing ℰ fib
+
+  left-adjoint-base-change→opfibration
+    : (L : ∀ {x y} → (f : Hom x y) → Functor (Fibre ℰ x) (Fibre ℰ y))
+    → (∀ {x y} → (f : Hom x y) → (L f ⊣ base-change f)) 
+    → Cocartesian-fibration
+  left-adjoint-base-change→opfibration L adj =
+    cartesian+weak-opfibration→opfibration fib $
+    hom-iso→weak-opfibration L λ u →
+      fibration→hom-iso-from fib u ni∘ (adjunct-hom-iso-from (adj u) _ ni⁻¹)
+```
+
+With some repackaging, we can see that this yields a bifibration.
+
+```agda
+  left-adjoint-base-change→bifibration
+    : (L : ∀ {x y} → (f : Hom x y) → Functor (Fibre ℰ x) (Fibre ℰ y))
+    → (∀ {x y} → (f : Hom x y) → (L f ⊣ base-change f))
+    → is-bifibration
+  left-adjoint-base-change→bifibration L adj .is-bifibration.fibration =
+    fib
+  left-adjoint-base-change→bifibration L adj .is-bifibration.opfibration =
+    left-adjoint-base-change→opfibration L adj
+```
diff --git a/src/Cat/Displayed/Cartesian.lagda.md b/src/Cat/Displayed/Cartesian.lagda.md
index d60e8ffb8..b8876109d 100644
--- a/src/Cat/Displayed/Cartesian.lagda.md
+++ b/src/Cat/Displayed/Cartesian.lagda.md
@@ -147,6 +147,38 @@ composite, rather than displayed directly over a composite.
     ·· ap (coe1→0 (λ i → Hom[ q i ] u′ a′)) (sym (unique m₂′ (from-pathp⁻ β)))
 ```
 
+Furthermore, if $f'' : a'' \to_{f} b'$ is also displayed over $f$,
+there's a unique vertical map $a'' \to a'$. This witnesses the fact that
+every cartesian map is [weakly cartesian].
+
+[weakly cartesian]: Cat.Displayed.Cartesian.Weak.html
+
+```agda
+  universalv : ∀ {a″} (f″ : Hom[ f ] a″ b′) → Hom[ id ] a″ a′
+  universalv f″ = universal′ (idr _) f″
+
+  commutesv
+    : ∀ {x′} → (g′ : Hom[ f ] x′ b′)
+    → f′ ∘′ universalv g′ ≡[ idr _ ] g′
+  commutesv = commutesp (idr _)
+
+  uniquev
+    : ∀ {x′} {g′ : Hom[ f ] x′ b′}
+    → (h′ : Hom[ id ] x′ a′)
+    → f′ ∘′ h′ ≡[ idr _ ] g′
+    → h′ ≡ universalv g′
+  uniquev h′ p = uniquep (idr f) refl (idr f) h′ p
+
+  uniquev₂
+    : ∀ {x′} {g′ : Hom[ f ] x′ b′}
+    → (h′ h″ : Hom[ id ] x′ a′)
+    → f′ ∘′ h′ ≡[ idr _ ] g′
+    → f′ ∘′ h″ ≡[ idr _ ] g′
+    → h′ ≡ h″
+  uniquev₂ h′ h″ p q =
+    uniquep₂ (idr f) refl (idr f) h′ h″ p q
+```
+
 ## Properties of Cartesian Morphisms
 
 The composite of 2 cartesian morphisms is in turn cartesian.
@@ -397,6 +429,35 @@ vertical+cartesian→invertible {x′ = x′} {x″ = x″} {f′ = f′} f-cart
       hom[] id′ ∎
 ```
 
+Furthermore, $f' : x' \to_{f} y'$ is cartesian if and only if the
+function $f \cdot' -$ is an equivalence.
+
+```agda
+postcompose-equiv→cartesian
+  : ∀ {x y x′ y′} {f : Hom x y}
+  → (f′ : Hom[ f ] x′ y′)
+  → (∀ {w w′} {g : Hom w x} → is-equiv {A = Hom[ g ] w′ x′} (f′ ∘′_))
+  → is-cartesian f f′
+postcompose-equiv→cartesian f′ eqv .is-cartesian.universal m h′ =
+  equiv→inverse eqv h′
+postcompose-equiv→cartesian f′ eqv .is-cartesian.commutes m h′ =
+  equiv→counit eqv h′
+postcompose-equiv→cartesian f′ eqv .is-cartesian.unique m′ p =
+  sym (equiv→unit eqv m′) ∙ ap (equiv→inverse eqv) p
+
+cartesian→postcompose-equiv
+  : ∀ {x y z x′ y′ z′} {f : Hom y z} {g : Hom x y} {f′ : Hom[ f ] y′ z′}
+  → is-cartesian f f′
+  → is-equiv {A = Hom[ g ] x′ y′} (f′ ∘′_)
+cartesian→postcompose-equiv cart =
+  is-iso→is-equiv $
+    iso (universal _)
+        (commutes _)
+        (λ g′ → sym (unique g′ refl))
+  where open is-cartesian cart
+```
+
+
 ## Cartesian Lifts
 
 We call an object $a'$ over $a$ together with a Cartesian arrow $f' : a'
@@ -436,6 +497,23 @@ record Cartesian-fibration : Type (o ⊔ ℓ ⊔ o′ ⊔ ℓ′) where
     Cartesian-lift (has-lift f y′)
 ```
 
+Note that if $\cE$ is a fibration, we can define an operation that
+allows us to move vertical morphisms between fibres. This actually
+extends to a collection of functors, called [base change functors].
+This operation is also definable for [weak fibrations], as it only
+uses the universal property that yields a vertical morphism.
+
+[base change functors]: Cat.Displayed.Cartesian.Indexing.html
+[weak fibrations]: Cat.Displayed.Cartesian.Weak.html#is-weak-cartesian-fibration
+
+```agda
+  rebase : ∀ {x y y′ y″} → (f : Hom x y)
+           → Hom[ id ] y′ y″
+           → Hom[ id ] (has-lift.x′ f y′) (has-lift.x′ f y″)
+  rebase f vert =
+    has-lift.universalv f _ (hom[ idl _ ] (vert ∘′ has-lift.lifting f _))
+```
+
 A Cartesian fibration is a displayed category having Cartesian lifts for
 every right corner.
 
@@ -472,24 +550,3 @@ fibre over a ring $R$ is the category of $R$-modules, Cartesian lifts
 are given by restriction of scalars.
 
 [category of modules]: Algebra.Ring.Module.html
-
-## Properties of Cartesian Fibrations
-
-If $\cE$ is a fibration, then every morphism is equivalent to
-a vertical morphism.
-
-```agda
-open Cartesian-lift
-open Cartesian-fibration
-
-fibration→vertical-equiv
-  : ∀ {X Y X′ Y′}
-  → (fib : Cartesian-fibration)
-  → (u : Hom X Y)
-  → Hom[ u ] X′ Y′ ≃ Hom[ id ] X′ (fib .has-lift u Y′ .x′)
-fibration→vertical-equiv fib u = Iso→Equiv $
-  (λ u′ → fib .has-lift _ _ .universal id (hom[ idr u ]⁻ u′)) ,
-  iso (λ u′ → hom[ idr u ] (fib .has-lift _ _ .lifting ∘′ u′))
-      (λ u′ → sym $ fib .has-lift _ _ .unique u′ (sym (hom[]-∙ _ _ ∙ liberate _)))
-      (λ u′ → (hom[]⟩⟨ fib .has-lift _ _ .commutes _ _) ·· hom[]-∙ _ _ ·· liberate _)
-```
diff --git a/src/Cat/Displayed/Cartesian/Indexing.lagda.md b/src/Cat/Displayed/Cartesian/Indexing.lagda.md
index 1f0aad341..8911fd4eb 100644
--- a/src/Cat/Displayed/Cartesian/Indexing.lagda.md
+++ b/src/Cat/Displayed/Cartesian/Indexing.lagda.md
@@ -54,31 +54,24 @@ of base_ along $f$.
 module _ {𝒶 𝒷} (f : Hom 𝒶 𝒷) where
   base-change : Functor (Fibre E 𝒷) (Fibre E 𝒶)
   base-change .F₀ ob = has-lift f ob .x′
-  base-change .F₁ {x} {y} vert = has-lift f y .universal id $
-    hom[ id-comm-sym ] (vert ∘′ has-lift f x .lifting)
+  base-change .F₁ {x} {y} vert = rebase f vert
 ```
 
 <!--
 ```agda
-  base-change .F-id {x} = sym $
-    has-lift f x .unique id′ (
-        sym (from-pathp (symP (idr′ _)))
-      ∙ sym (ap hom[] (sym (from-pathp (symP (idl′ _))))
-      ·· hom[]-∙ _ _ ·· reindex _ _))
-
-  base-change .F-∘ {x} {y} {z} f′ g′ = sym $ has-lift f z .unique _
-    (  pulll-indexr _ (has-lift f z .commutes _ _)
-    ·· ap hom[] (
-        whisker-l _ ∙ ap hom[] (
-          sym (from-pathp (assoc′ _ _ _))
-        ∙ ap hom[] (ap (f′ ∘′_) (has-lift f y .commutes _ _))))
-    ·· hom[]-∙ _ _ ·· hom[]-∙ _ _
-    ·· ap hom[] (
-        whisker-r _
-      ∙ ap hom[] (sym (from-pathp (symP (assoc′ _ _ _)))))
-    ·· hom[]-∙ _ _ ·· hom[]-∙ _ _
-    ·· reindex _ (ap (_∘ _) (idl id) ∙ id-comm-sym)
-    ·· sym (hom[]-∙ _ _) ∙ ap hom[] (sym (whisker-l _)))
+  base-change .F-id {x} =
+    sym $ has-lift.uniquev _ _ _ $ to-pathp $
+      idr[] ∙ (sym $ cancel _ _ (idl′ _))
+
+  base-change .F-∘ {x} {y} {z} f′ g′ =
+    sym $ has-lift.uniquev _ _ _ $ to-pathp $
+      smashr _ _
+      ·· revive₁ (pulll[] (idr f) (has-lift.commutesv _ _ _))
+      ·· smashl _ _
+      ·· revive₁ (pullr[] (idr f) (has-lift.commutesv _ _ _))
+      ·· smashr _ _
+      ·· assoc[]
+      ·· sym (smashl _ _)
 ```
 -->
 
@@ -101,20 +94,14 @@ of heart. </summary>
   base-change-id = to-natural-iso mi where
     open make-natural-iso
     mi : make-natural-iso (base-change id) Id
-    mi .eta x = has-lift id x .lifting
-    mi .inv x = has-lift id x .universal _ (hom[ sym (idl id) ] id′)
-    mi .eta∘inv x =
-        ap hom[] (has-lift id x .commutes _ _)
-      ·· hom[]-∙ _ _ ·· reindex _ _ ∙ transport-refl id′
+    mi .eta x = has-lift.lifting id x
+    mi .inv x = has-lift.universalv id x id′
+    mi .eta∘inv x = cancel _ _ (has-lift.commutesv _ _ _)
     mi .inv∘eta x = sym $
-        has-lift id x .unique Fa.id (shiftr (idr _) (idr′ _))
-      ∙ sym (has-lift id x .unique _ (pulll-indexr _ (has-lift id x .commutes _ _)
-      ·· ap hom[] (whisker-l _
-      ·· reindex _ (idl _ ∙ sym (idr _) ∙ ap (_∘ id) (sym (idr _)))
-      ·· sym (hom[]-∙ _ _) ∙ ap hom[] (from-pathp (idl′ _)))
-      ·· hom[]-∙ _ _ ∙ reindex _ _))
-    mi .natural x y f = ap hom[] (sym (has-lift id y .commutes _ _) ∙ ap₂ _∘′_ refl
-      (ap (has-lift id y .universal _) (sym (reindex _ refl ∙ transport-refl _))))
+      has-lift.uniquev₂ id x Fa.id _ (cast[] $ idr′ _) $
+      to-pathp (smashr _ _ ∙ cancel _ _ (cancell[] _ (has-lift.commutesv _ _ _)))
+    mi .natural x y f = ap hom[] $ sym $
+      has-lift.commutes _ _ _ _ ·· hom[]-∙ _ _ ·· liberate _
 ```
 </details>
 
@@ -138,47 +125,43 @@ properties and I recommend that nobody look at it, ever. </summary>.
   base-change-comp = to-natural-iso mi where
     open make-natural-iso
     mi : make-natural-iso (base-change (f ∘ g)) (base-change g F∘ base-change f)
-    mi .eta x = has-lift g _ .universal _ $
-      has-lift f _ .universal _ $
-        hom[ ap (f ∘_) (sym (idr g)) ] (has-lift (f ∘ g) x .lifting)
-    mi .inv x = has-lift (f ∘ g) _ .universal _ $
-      hom[ sym (idr _) ] (has-lift f _ .lifting ∘′ has-lift g _ .lifting)
-    mi .eta∘inv x = sym $
-        has-lift g _ .unique _ (shiftr (idr _) (idr′ _))
-      ∙ sym (has-lift g _ .unique _ (pulll-indexr _ (has-lift g _ .commutes _ _)
-      ∙ has-lift f _ .unique _ (pulll-indexr _ (has-lift f _ .commutes _ _)
-      ∙ ap hom[] (whisker-l _ ∙ ap hom[] (has-lift (f ∘ g) _ .commutes _ _))
-      ∙ hom[]-∙ _ _ ∙ hom[]-∙ _ _) ∙ sym (has-lift f x .unique _
-      (whisker-r _ ∙ reindex _ _))))
-    mi .inv∘eta x = sym $
-        has-lift (f ∘ g) _ .unique _ (sym (from-pathp (symP (idr′ _))))
-      ∙ sym (has-lift (f ∘ g) _ .unique _ (pulll-indexr _
-          (has-lift (f ∘ g) _ .commutes _ _)
-      ∙ ap hom[] (whisker-l _ ∙ ap hom[] (sym (from-pathp (assoc′ _ _ _))
-      ∙ ap hom[] (ap₂ _∘′_ refl (has-lift g _ .commutes _ _)
-      ∙ has-lift f _ .commutes _ _)))
-      ∙ hom[]-∙ _ _ ∙ hom[]-∙ _ _ ∙ hom[]-∙ _ _ ∙ reindex _ _))
-    mi .natural x y f′ = ap hom[]
-      (has-lift g (has-lift f y .x′) .unique _
-        (sym (from-pathp (symP (assoc′ _ _ _ )))
-        ·· ap hom[ sym (assoc _ _ _) ] (ap₂ _∘′_ (has-lift g _ .commutes id _) refl)
-        ·· ap hom[ sym (assoc _ _ _) ] (whisker-l _)
-        ·· hom[]-∙ _ _
-        ·· ap hom[] (sym (from-pathp (assoc′ (F₁ (base-change f) f′)
-          (has-lift g _ .lifting) (has-lift g _ .universal _ _)))
-        ∙ ap hom[] (ap₂ _∘′_ refl (has-lift g _ .commutes _ _)))
-        ∙ hom[]-∙ _ _ ∙ reindex _ (idl _ ∙ ap (g ∘_) (sym (idl id))))
-      ) ∙ ap hom[]
-      ( sym (has-lift g _ .unique _ (sym (from-pathp (symP (assoc′ _ _ _)))
-      ∙ ap hom[ sym (assoc _ _ _) ] (ap₂ _∘′_ (has-lift g _ .commutes _ _) refl)
-      ∙ sym (has-lift f y .unique _ (pulll-indexr _ (has-lift f y .commutes _ _)
-        ∙ ap hom[] (whisker-l _ ∙ ap hom[] (sym (from-pathp (assoc′ _ _ _))
-        ∙ ap hom[] (ap₂ _∘′_ refl (has-lift f x .commutes _ _))) ∙ hom[]-∙ _ _)
-        ∙ hom[]-∙ _ _ ∙ ap hom[] (whisker-r _)
-        ∙ reindex _ (idl _ ∙ ap (f ∘_) (ap (g ∘_) (sym (idl id)))))
-        ∙ sym (has-lift f y .unique _ (pulll-indexr _ (has-lift f y .commutes _ _)
-        ∙ ap hom[] (whisker-l  _) ∙ hom[]-∙ _ _
-        ∙ ap hom[] (has-lift (f ∘ g) y .commutes _ _) ∙ hom[]-∙ _ _
-        ∙ sym (hom[]-∙ _ _ ∙ reindex _ _)))))))
+    mi .eta x =
+      has-lift.universalv g _ $ has-lift.universal f x g (has-lift.lifting (f ∘ g) x)
+    mi .inv x =
+      has-lift.universalv (f ∘ g) x (has-lift.lifting f _ ∘′ has-lift.lifting g _)
+    mi .eta∘inv x =
+      has-lift.uniquev₂ g _ _ _
+        (to-pathp $
+          smashr _ _
+          ·· revive₁ (pulll[] _ (has-lift.commutesv g _ _))
+          ·· has-lift.uniquep₂ f _ refl refl refl _ _
+            (pulll-indexr _ (has-lift.commutes f _ _ _)
+            ∙ cancel _ _ (has-lift.commutesv (f ∘ g) _ _))
+            refl)
+        (idr′ _)
+    mi .inv∘eta x =
+      has-lift.uniquev₂ (f ∘ g) _ _ _
+        (to-pathp $
+          smashr _ _
+          ·· revive₁ (pulll[] _ (has-lift.commutesv (f ∘ g) _ _))
+          ·· revive₁ (pullr[] _ (has-lift.commutesv g _ _))
+          ∙ cancel _ _ (has-lift.commutes f _ _ _))
+        (idr′ _)
+    mi .natural x y f′ =
+      ap hom[] $ cartesian→weak-monic E (has-lift.cartesian g _) _ _ $
+        from-pathp⁻ (pulll[] _ (has-lift.commutes g _ _ _))
+        ·· smashl _ _ ·· smashl _ _
+        ·· revive₁ (pullr[] _ (has-lift.commutesv g _ _ ))
+        ·· (cartesian→weak-monic E (has-lift.cartesian f _) _ _ $
+          whisker-r _
+          ·· revive₁ (pulll[] _ (has-lift.commutesv f _ _))
+          ·· smashl _ _
+          ·· revive₁ (pullr[] _ (has-lift.commutes f _ _ _))
+          ·· duplicate _ (ap (f ∘_) (intror (idl id))) _
+          ·· revive₁ (symP (has-lift.commutesv (f ∘ g) _ _))
+          ·· revive₁ (pushl[] _ (symP $ has-lift.commutes f _ _ _))
+          ·· unwhisker-r _ (ap (g ∘_) (sym $ idl id))
+          ·· ap (has-lift.lifting f _ ∘′_) (expandl _ _ ∙ reindex _ _))
+        ∙ cancel (sym $ assoc _ _ _) _ (pushl[] _ (symP $ has-lift.commutes g _ _ _))
 ```
 </details>
diff --git a/src/Cat/Displayed/Cartesian/Weak.lagda.md b/src/Cat/Displayed/Cartesian/Weak.lagda.md
index 65d5c4eef..c2696eb45 100644
--- a/src/Cat/Displayed/Cartesian/Weak.lagda.md
+++ b/src/Cat/Displayed/Cartesian/Weak.lagda.md
@@ -1,25 +1,36 @@
 ```agda
 open import Cat.Displayed.Base
 open import Cat.Displayed.Fibre
+open import Cat.Functor.Hom
+open import Cat.Functor.Hom.Displayed
+open import Cat.Instances.Functor
+open import Cat.Instances.Product
 open import Cat.Prelude
 
 import Cat.Displayed.Cartesian as Cart
+import Cat.Displayed.Cartesian.Indexing as Indexing
 import Cat.Displayed.Reasoning as DR
 import Cat.Displayed.Morphism as DM
+import Cat.Reasoning as CR
 
 module Cat.Displayed.Cartesian.Weak
   {o ℓ o′ ℓ′}
   {ℬ : Precategory o ℓ}
   (ℰ : Displayed ℬ o′ ℓ′)
   where
+```
 
-open Precategory ℬ
+<!--
+```agda
+open CR ℬ
 open Displayed ℰ
 open Cart ℰ
 open DR ℰ
 open DM ℰ
 open Functor
+open Functor
 ```
+-->
 
 # Weak Cartesian Morphisms
 
@@ -62,6 +73,8 @@ record is-weak-cartesian
                 → (h′ : Hom[ id ] x′ a′)
                 → f′ ∘′ h′ ≡[ idr _ ] g′
                 → h′ ≡ universal g′
+
+open is-weak-cartesian
 ```
 
 Like their stronger counterparts, weak cartesian lifts are unique
@@ -115,12 +128,12 @@ cartesian→weak-cartesian {f = f} {f′ = f′} cart = weak-cart where
   open is-cartesian cart
 
   weak-cart : is-weak-cartesian f f′
-  weak-cart .is-weak-cartesian.universal g′ =
-    universal′ (idr f) g′
-  weak-cart .is-weak-cartesian.commutes g′ =
-    commutesp (idr f) g′
-  weak-cart .is-weak-cartesian.unique h′ p =
-    uniquep (idr f) refl (idr f) h′ p
+  weak-cart .universal g′ =
+    universalv g′
+  weak-cart .commutes g′ =
+    commutesv g′
+  weak-cart .unique h′ p =
+    uniquev h′ p
 ```
 
 Furthermore, if $\cE$ is a fibration, weakly cartesian morphisms are
@@ -141,13 +154,13 @@ weak-cartesian→cartesian {x = x} {y′ = y′} {f = f} {f′ = f′} fib f-wea
   module f-weak = is-weak-cartesian f-weak
 
   x* : Ob[ x ]
-  x* = Cartesian-lift.x′ (has-lift f y′)
+  x* = has-lift.x′ f y′
 
   f* : Hom[ f ] x* y′
-  f* = Cartesian-lift.lifting (has-lift f y′)
+  f* = has-lift.lifting f y′
 
   f*-cart : is-cartesian f f*
-  f*-cart = Cartesian-lift.cartesian (has-lift f y′)
+  f*-cart = has-lift.cartesian f y′
 
   f*-weak : is-weak-cartesian f f*
   f*-weak = cartesian→weak-cartesian f*-cart
@@ -159,6 +172,33 @@ weak-cartesian→cartesian {x = x} {y′ = y′} {f = f} {f′ = f′} fib f-wea
       (f-weak.commutes f*)
 ```
 
+$f' : x' \to_{f} y'$ is a weak cartesian morphism if and only if
+postcomposition of $f'$ onto vertical maps is an equivalence.
+
+```agda
+postcompose-equiv→weak-cartesian
+  : ∀ {x y x′ y′} {f : Hom x y}
+  → (f′ : Hom[ f ] x′ y′)
+  → (∀ {x″} → is-equiv {A = Hom[ id ] x″ x′} (f′ ∘′_))
+  → is-weak-cartesian f f′
+postcompose-equiv→weak-cartesian f′ eqv .universal h′ =
+  equiv→inverse eqv (hom[ idr _ ]⁻ h′)
+postcompose-equiv→weak-cartesian f′ eqv .commutes h′ =
+  to-pathp⁻ (equiv→counit eqv (hom[ idr _ ]⁻ h′))
+postcompose-equiv→weak-cartesian f′ eqv .unique m′ p =
+  (sym $ equiv→unit eqv m′) ∙ ap (equiv→inverse eqv) (from-pathp⁻ p)
+
+weak-cartesian→postcompose-equiv
+  : ∀ {x y x′ x″ y′} {f : Hom x y} {f′ : Hom[ f ] x′ y′}
+  → is-weak-cartesian f f′
+  → is-equiv {A = Hom[ id ] x″ x′} (f′ ∘′_)
+weak-cartesian→postcompose-equiv wcart =
+  is-iso→is-equiv $
+    iso (λ h′ → wcart .universal (hom[ idr _ ] h′))
+        (λ h′ → from-pathp⁻ (wcart .commutes _) ·· hom[]-∙ _ _ ·· liberate _)
+        (λ h′ → sym $ wcart .unique _ (to-pathp refl))
+```
+
 ## Weak Cartesian Lifts
 
 We can also define a notion of weak cartesian lifts, much like we can
@@ -178,24 +218,88 @@ record Weak-cartesian-lift
 ```
 
 A displayed category that has weak cartesian lifts for all morphisms
-in the base is called a **prefibered category**. Notably, prefibered
-categories are fibred when weak cartesian morphisms are closed under
-composition.
+in the base is called a **weak cartesian fibration**, though we will
+often use the term **weak fibration**. Other authors call weak
+fibrations **prefibred categories**, though we avoid this name as it
+conflicts with the precategory/category distinction.
 
 ```agda
-weak-cartesian-lifts→fibration
-  : (lifts : ∀ {x y} → (f : Hom x y) → (y′ : Ob[ y ]) → Weak-cartesian-lift f y′)
-  → (∀ {x y z x′ y′ z′} {f : Hom y z} {g : Hom x y}
-     → {f′ : Hom[ f ] y′ z′} {g′ : Hom[ g ] x′ y′}
-     → is-weak-cartesian f f′ → is-weak-cartesian g g′
-     → is-weak-cartesian (f ∘ g) (f′ ∘′ g′))
-  → Cartesian-fibration
-weak-cartesian-lifts→fibration weak-lift weak-∘ .Cartesian-fibration.has-lift {x = x} f y′ = f-lift where
+record is-weak-cartesian-fibration : Type (o ⊔ ℓ ⊔ o′ ⊔ ℓ′) where
+  no-eta-equality
+  field
+    weak-lift : ∀ {x y} → (f : Hom x y) → (y′ : Ob[ y ]) → Weak-cartesian-lift f y′
 
   module weak-lift {x y} (f : Hom x y) (y′ : Ob[ y ]) =
     Weak-cartesian-lift (weak-lift f y′)
-  module weak-∘ {x y z} (f : Hom y z) (g : Hom x y) (z′ : Ob[ z ]) =
-    is-weak-cartesian (weak-∘ (weak-lift.weak-cartesian f z′) (weak-lift.weak-cartesian g _))
+```
+
+Note that if $\cE$ is a weak fibration, we can define an operation that
+allows us to move vertical morphisms between fibres. This is actually
+enough to define [base change functors], though they are not well behaved
+unless $\cE$ is a fibration.
+
+[base change functors]: Cat.Displayed.Cartesian.Indexing.html
+
+```agda
+  rebase : ∀ {x y y′ y″} → (f : Hom x y)
+           → Hom[ id ] y′ y″
+           → Hom[ id ] (weak-lift.x′ f y′) (weak-lift.x′ f y″)
+  rebase f vert =
+    weak-lift.universal f _ (hom[ idl _ ] (vert ∘′ weak-lift.lifting f _))
+```
+
+Every fibration is a weak fibration.
+
+```agda
+cartesian-lift→weak-cartesian-lift
+  : ∀ {x y} {f : Hom x y} {y′ : Ob[ y ]}
+  → Cartesian-lift f y′
+  → Weak-cartesian-lift f y′
+
+fibration→weak-fibration
+  : Cartesian-fibration
+  → is-weak-cartesian-fibration
+```
+
+<details>
+<summary>The proofs of these facts are just shuffling around data, so we
+omit them.
+</summary>
+```agda
+cartesian-lift→weak-cartesian-lift cart .Weak-cartesian-lift.x′ =
+  Cartesian-lift.x′ cart
+cartesian-lift→weak-cartesian-lift cart .Weak-cartesian-lift.lifting =
+  Cartesian-lift.lifting cart
+cartesian-lift→weak-cartesian-lift cart .Weak-cartesian-lift.weak-cartesian =
+  cartesian→weak-cartesian (Cartesian-lift.cartesian cart)
+
+fibration→weak-fibration fib .is-weak-cartesian-fibration.weak-lift x y′ =
+  cartesian-lift→weak-cartesian-lift (Cartesian-fibration.has-lift fib x y′)
+```
+</details>
+
+
+Notably, weak fibrations are fibrations when weak cartesian morphisms
+are closed under composition.
+
+```agda
+module _ where
+  open Cartesian-fibration
+  open is-cartesian
+
+  weak-fibration→fibration
+    : is-weak-cartesian-fibration
+    → (∀ {x y z x′ y′ z′} {f : Hom y z} {g : Hom x y}
+       → {f′ : Hom[ f ] y′ z′} {g′ : Hom[ g ] x′ y′}
+       → is-weak-cartesian f f′ → is-weak-cartesian g g′
+       → is-weak-cartesian (f ∘ g) (f′ ∘′ g′))
+    → Cartesian-fibration
+  weak-fibration→fibration weak-fib weak-∘ .has-lift {x = x} f y′ = f-lift where
+    open is-weak-cartesian-fibration weak-fib
+  
+    module weak-∘ {x y z} (f : Hom y z) (g : Hom x y) (z′ : Ob[ z ]) =
+      is-weak-cartesian (weak-∘ (weak-lift.weak-cartesian f z′)
+                                (weak-lift.weak-cartesian g _))
 ```
 
 To show that $f$ has a cartesian lift, we begin by taking the weak
@@ -214,16 +318,16 @@ cartesian lift $f^{*}$ of $f$.
 ~~~
 
 ```agda
-  x* : Ob[ x ]
-  x* = weak-lift.x′ f y′
-
-  f* : Hom[ f ] x* y′
-  f* = weak-lift.lifting f y′
-
-  f*-weak-cartesian : is-weak-cartesian f f*
-  f*-weak-cartesian = weak-lift.weak-cartesian f y′
-
-  module f* = is-weak-cartesian (f*-weak-cartesian)
+    x* : Ob[ x ]
+    x* = weak-lift.x′ f y′
+  
+    f* : Hom[ f ] x* y′
+    f* = weak-lift.lifting f y′
+  
+    f*-weak-cartesian : is-weak-cartesian f f*
+    f*-weak-cartesian = weak-lift.weak-cartesian f y′
+  
+    module f* = is-weak-cartesian (f*-weak-cartesian)
 ```
 
 We must now show that the weak cartesian morphism $f^{*}$ is actually
@@ -255,28 +359,28 @@ morphism $u' \to u^{*}$, which we can then compose with $m^{*}$
 to obtain the requisite map.
 
 ```agda
-  module Morphisms
-    {u : Ob} {u′ : Ob[ u ]} (m : Hom u x) (h′ : Hom[ f ∘ m ] u′ y′)
-    where
-      u* : Ob[ u ]
-      u* = weak-lift.x′ m _
-
-      m* : Hom[ m ] u* x*
-      m* = weak-lift.lifting m _
-
-      m*-weak-cartesian : is-weak-cartesian m m*
-      m*-weak-cartesian = weak-lift.weak-cartesian m x*
-
-      module m* = is-weak-cartesian m*-weak-cartesian
-      module f*∘m* = is-weak-cartesian (weak-∘ f*-weak-cartesian m*-weak-cartesian)
+    module Morphisms
+      {u : Ob} {u′ : Ob[ u ]} (m : Hom u x) (h′ : Hom[ f ∘ m ] u′ y′)
+      where
+        u* : Ob[ u ]
+        u* = weak-lift.x′ m _
+  
+        m* : Hom[ m ] u* x*
+        m* = weak-lift.lifting m _
+  
+        m*-weak-cartesian : is-weak-cartesian m m*
+        m*-weak-cartesian = weak-lift.weak-cartesian m x*
+  
+        module m* = is-weak-cartesian m*-weak-cartesian
+        module f*∘m* = is-weak-cartesian (weak-∘ f*-weak-cartesian m*-weak-cartesian)
 ```
 
 
 ```agda
-  f*-cartesian : is-cartesian f f*
-  f*-cartesian .is-cartesian.universal {u = u} {u′ = u′} m h′ =
-    hom[ idr m ] (m* ∘′  f*∘m*.universal h′)
-    where open Morphisms m h′
+    f*-cartesian : is-cartesian f f*
+    f*-cartesian .universal {u = u} {u′ = u′} m h′ =
+      hom[ idr m ] (m* ∘′  f*∘m*.universal h′)
+      where open Morphisms m h′
 ```
 
 <details>
@@ -285,18 +389,18 @@ yoga; the only real mathematical content is that the factorization of
 $h'$ via $f^{*} \cdot m^{*}$ commutes.
 </summary>
 ```agda
-  f*-cartesian .is-cartesian.commutes {u = u} {u′ = u′} m h′ = path
-    where
-      open Morphisms m h′
-
-      abstract
-        path : f* ∘′ hom[ idr m ] (m* ∘′ f*∘m*.universal h′) ≡ h′
-        path =
-          f* ∘′ hom[] (m* ∘′ f*∘m*.universal h′)   ≡⟨ whisker-r _ ⟩
-          hom[] (f* ∘′ m* ∘′ f*∘m*.universal h′)   ≡⟨ assoc[] {q = idr _} ⟩
-          hom[] ((f* ∘′ m*) ∘′ f*∘m*.universal h′) ≡⟨ hom[]⟩⟨ from-pathp⁻ (f*∘m*.commutes h′) ⟩
-          hom[] (hom[] h′)                         ≡⟨ hom[]-∙ _ _ ∙ liberate _ ⟩
-          h′                                       ∎
+    f*-cartesian .commutes {u = u} {u′ = u′} m h′ = path
+      where
+        open Morphisms m h′
+  
+        abstract
+          path : f* ∘′ hom[ idr m ] (m* ∘′ f*∘m*.universal h′) ≡ h′
+          path =
+            f* ∘′ hom[] (m* ∘′ f*∘m*.universal h′)   ≡⟨ whisker-r _ ⟩
+            hom[] (f* ∘′ m* ∘′ f*∘m*.universal h′)   ≡⟨ assoc[] {q = idr _} ⟩
+            hom[] ((f* ∘′ m*) ∘′ f*∘m*.universal h′) ≡⟨ hom[]⟩⟨ from-pathp⁻ (f*∘m*.commutes h′) ⟩
+            hom[] (hom[] h′)                         ≡⟨ hom[]-∙ _ _ ∙ liberate _ ⟩
+            h′                                       ∎
 ```
 </details>
 
@@ -306,25 +410,25 @@ the fact that both $m^{*}$ and $f^{*} \cdot m^{*}$ are weak cartesian
 maps.
 </summary>
 ```agda
-  f*-cartesian .is-cartesian.unique {u = u} {u′ = u′} {m = m} {h′ = h′} m′ p = path
-    where
-      open Morphisms m h′
-
-      abstract
-        universal-path : (f* ∘′ m*) ∘′ m*.universal m′ ≡[ idr (f ∘ m) ] h′
-        universal-path = to-pathp $
-          hom[] ((f* ∘′ m*) ∘′ m*.universal m′) ≡˘⟨ assoc[] {p = ap (f ∘_) (idr m)} ⟩
-          hom[] (f* ∘′ (m* ∘′ m*.universal m′)) ≡⟨ hom[]⟩⟨ ap (f* ∘′_) (from-pathp⁻ (m*.commutes m′)) ⟩
-          hom[] (f* ∘′ hom[] m′)                ≡⟨ smashr _ _ ∙ liberate _ ⟩
-          f* ∘′ m′                              ≡⟨ p ⟩
-          h′ ∎
-
-        path : m′ ≡ hom[ idr m ] (m* ∘′ f*∘m*.universal h′)
-        path =
-          m′                               ≡˘⟨ from-pathp (m*.commutes m′) ⟩
-          hom[] (m* ∘′ m*.universal m′)    ≡⟨ reindex _ (idr m) ⟩
-          hom[] (m* ∘′ m*.universal m′)    ≡⟨ hom[]⟩⟨ ap (m* ∘′_) (f*∘m*.unique _ universal-path) ⟩
-          hom[] (m* ∘′ f*∘m*.universal h′) ∎
+    f*-cartesian .unique {u = u} {u′ = u′} {m = m} {h′ = h′} m′ p = path
+      where
+        open Morphisms m h′
+  
+        abstract
+          universal-path : (f* ∘′ m*) ∘′ m*.universal m′ ≡[ idr (f ∘ m) ] h′
+          universal-path = to-pathp $
+            hom[] ((f* ∘′ m*) ∘′ m*.universal m′) ≡˘⟨ assoc[] {p = ap (f ∘_) (idr m)} ⟩
+            hom[] (f* ∘′ (m* ∘′ m*.universal m′)) ≡⟨ hom[]⟩⟨ ap (f* ∘′_) (from-pathp⁻ (m*.commutes m′)) ⟩
+            hom[] (f* ∘′ hom[] m′)                ≡⟨ smashr _ _ ∙ liberate _ ⟩
+            f* ∘′ m′                              ≡⟨ p ⟩
+            h′ ∎
+  
+          path : m′ ≡ hom[ idr m ] (m* ∘′ f*∘m*.universal h′)
+          path =
+            m′                               ≡˘⟨ from-pathp (m*.commutes m′) ⟩
+            hom[] (m* ∘′ m*.universal m′)    ≡⟨ reindex _ (idr m) ⟩
+            hom[] (m* ∘′ m*.universal m′)    ≡⟨ hom[]⟩⟨ ap (m* ∘′_) (f*∘m*.unique _ universal-path) ⟩
+            hom[] (m* ∘′ f*∘m*.universal h′) ∎
 ```
 </details>
 
@@ -332,76 +436,307 @@ Putting this all together, we can finally deduce that $f^{*}$ is
 a cartesian lift of $f$.
 
 ```agda
-  f-lift : Cartesian-lift f y′
-  f-lift .Cartesian-lift.x′ = x*
-  f-lift .Cartesian-lift.lifting = f*
-  f-lift .Cartesian-lift.cartesian = f*-cartesian
+    f-lift : Cartesian-lift f y′
+    f-lift .Cartesian-lift.x′ = x*
+    f-lift .Cartesian-lift.lifting = f*
+    f-lift .Cartesian-lift.cartesian = f*-cartesian
 ```
 
-<!--
-[TODO: Reed M, 25/01/2023] Explain this code when showing that left
-adjoints to reindexing gives opfibrations.
+## Factorisations in Weak Fibrations
+
+If $\cE$ is a weak fibration, then every morphism factorizes into
+a vertical morphism followed by a weak cartesian morphism.
+
 ```agda
-weak-cartesian-lift→reindex
-  : ∀ {x y} {f : Hom x y} {x′ : Ob[ x ]} {y′ : Ob[ y ]}
-  → (weak-lift : Weak-cartesian-lift f y′)
-  → Hom[ f ] x′ y′ ≃ Hom[ id ] x′ (Weak-cartesian-lift.x′ weak-lift)
-weak-cartesian-lift→reindex weak-lift = Iso→Equiv $
-  universal ,
-  iso (λ f′ → hom[ idr _ ] (lifting ∘′ f′))
-      (λ f′ → sym $ unique f′ (to-pathp refl))
-      (λ f′ → (hom[]⟩⟨ from-pathp⁻ (commutes f′)) ·· hom[]-∙ _ _ ·· liberate _)
+record weak-cartesian-factorisation
+  {x y x′ y′} {f : Hom x y}
+  (f′ : Hom[ f ] x′ y′)
+  : Type (o ⊔ ℓ ⊔ o′ ⊔ ℓ′)
   where
-    open Weak-cartesian-lift weak-lift
-
-module _ (U : ∀ {x y} → Hom x y → Functor (Fibre ℰ y) (Fibre ℰ x))
-         where
-
-  reindex-iso-natural
-    : (∀ {x y x′ y′} {f : Hom x y} → Hom[ f ] x′ y′ → Hom[ id ] x′ (U f .F₀ y′))
-    → Type _
-  reindex-iso-natural to =
-    ∀ {x y x′ x″ y′} {f : Hom x y}
-    → (f′ : Hom[ f ] x″ y′) (g′ : Hom[ id ] x′ x″)
-    → to (hom[ idr _ ] (f′ ∘′ g′)) ≡[ sym (idl id) ] to f′ ∘′ g′
-
-  reindex→weak-cartesian-lift
-    : (to : ∀ {x y x′ y′} {f : Hom x y} → Hom[ f ] x′ y′ → Hom[ id ] x′ (U f .F₀ y′))
-    → (eqv : ∀ {x y x′ y′} {f : Hom x y} → is-equiv (to {x} {y} {x′} {y′} {f}))
-    → (natural : reindex-iso-natural to)
-    → ∀ {x y y′} {f : Hom x y}
-    → Weak-cartesian-lift f y′
-  reindex→weak-cartesian-lift to to-eqv natural {y′ = y′} {f = f} = weak-lift where
-    open Weak-cartesian-lift
-    open is-weak-cartesian
+  no-eta-equality
+  field
+    {x″} : Ob[ x ]
+    vertical : Hom[ id ] x′ x″
+    weak-cart : Hom[ f ] x″ y′
+    has-weak-cartesian : is-weak-cartesian f weak-cart
+    factors : f′ ≡[ sym (idr _) ] weak-cart ∘′ vertical
+
+weak-fibration→weak-cartesian-factors
+  : ∀ {x y x′ y′} {f : Hom x y}
+  → is-weak-cartesian-fibration
+  → (f′ : Hom[ f ] x′ y′)
+  → weak-cartesian-factorisation f′
+```
+
+Because $\cE$ is a weak fibration, every morphism in $\cB$ has a weak
+cartesian lift. This allows us to take the lift of $f$, which will
+form the weak cartesian component of the factorisation. The vertical
+component can be obtained by taking the universal factorisation of
+$f'$ by the lift of $f$.
+
+```agda
+weak-fibration→weak-cartesian-factors {y′ = y′} {f = f} wfib f′ = weak-factor where
+  open is-weak-cartesian-fibration wfib
+  module f-lift = weak-lift f y′
+  open weak-cartesian-factorisation
+
+  weak-factor : weak-cartesian-factorisation f′
+  weak-factor .x″ = f-lift.x′
+  weak-factor .vertical = f-lift.universal f′
+  weak-factor .weak-cart = f-lift.lifting
+  weak-factor .has-weak-cartesian = f-lift.weak-cartesian
+  weak-factor .factors = symP $ f-lift.commutes f′
+```
+
+## Weak Fibrations and Equivalence of Hom Sets
+
+If $\cE$ is a weak fibration, then the hom sets $x' \to_f y'$ and
+$x' \to_{id} f^{*}(y')$ are equivalent, where $f^{*}(y')$ is the domain
+of the lift of $f$ along $y'$. To go from $f' : x' \to_u y'$ to
+$x' \to_{id} f^{*}(y')$, we use the vertical component of the
+factorisation of $f'$; this forms an equivalence, as this factorisation
+is unique.
 
-    from : ∀ {x y x′ y′} {f : Hom x y} → Hom[ id ] x′ (U f .F₀ y′) → Hom[ f ] x′ y′
-    from = equiv→inverse to-eqv
+```agda
+module _ (wfib : is-weak-cartesian-fibration) where
+  open is-weak-cartesian-fibration wfib
+
+  weak-fibration→universal-is-equiv
+    : ∀ {x y x′ y′}
+    → (f : Hom x y)
+    → is-equiv (weak-lift.universal f y′ {x′})
+  weak-fibration→universal-is-equiv {y′ = y′} f = is-iso→is-equiv $
+    iso (λ f′ → hom[ idr f ] (weak-lift.lifting f y′ ∘′ f′) )
+        (λ f′ → sym $ weak-lift.unique f y′ f′ (to-pathp refl))
+        (λ f′ → cancel _ _ (weak-lift.commutes f y′ f′))
+
+  weak-fibration→vertical-equiv
+    : ∀ {x y x′ y′}
+    → (f : Hom x y)
+    → Hom[ f ] x′ y′ ≃ Hom[ id ] x′ (weak-lift.x′ f y′)
+  weak-fibration→vertical-equiv {y′ = y′} f =
+    weak-lift.universal f y′ ,
+    weak-fibration→universal-is-equiv f
+```
+
+Furthermore, this equivalence can be extended into a natural isomorphism
+between $\cE_{u}(-,y')$ and $\cE_{x}(-,u^{*}(y'))$.
+
+```agda
+  weak-fibration→hom-iso-into
+    : ∀ {x y y′} (u : Hom x y)
+    → natural-iso (Hom-over-into ℰ u y′) (Hom-into (Fibre ℰ x) (weak-lift.x′ u y′))
+  weak-fibration→hom-iso-into {x} {y} {y′} u = to-natural-iso mi where
+    open make-natural-iso
+
+    u*y′ : Ob[ x ]
+    u*y′ = weak-lift.x′ u y′
+   
+    mi : make-natural-iso (Hom-over-into ℰ u y′) (Hom-into (Fibre ℰ x) u*y′)
+    mi .eta x u′ = weak-lift.universal u y′ u′
+    mi .inv x v′ = hom[ idr u ] (weak-lift.lifting u y′ ∘′ v′)
+    mi .eta∘inv x = funext λ v′ →
+      sym $ weak-lift.unique u _ _ (to-pathp refl)
+    mi .inv∘eta x = funext λ u′ →
+      from-pathp (weak-lift.commutes u _ _)
+    mi .natural x y v′ = funext λ u′ →
+      weak-lift.unique u _ _ $ to-pathp $
+        smashr _ _
+        ∙ weave _ (ap (u ∘_) (idl id)) _ (pulll′ _ (weak-lift.commutes _ _ _))
+```
 
-    from-natural
+An *extremely* useful fact is that the converse is true: if there is some
+lifting of objects $\cE_{y} \to \cE_{x}$ for every morphism $f : x \to y$
+in $\cB$, along with a natural equivalence of homs as above, then
+$\cE$ is a weak fibration.
+
+This result is the primary reason to care about weak fibrations, as we
+already have a toolkit for constructing natural equivalences of
+hom sets! Most notably, this allows us to use the theory of [adjuncts]
+to construct weak fibrations.
+
+[adjuncts]: Cat.Functor.Adjoint.html#adjuncts
+
+```agda
+module _ (_*₀_ : ∀ {x y} → Hom x y → Ob[ y ] → Ob[ x ]) where
+  open is-weak-cartesian-fibration
+  open Weak-cartesian-lift
+  open is-weak-cartesian
+
+  private
+    vertical-equiv-iso-natural
+      : (∀ {x y x′ y′} {f : Hom x y} → Hom[ f ] x′ y′ → Hom[ id ] x′ (f *₀ y′))
+      → Type _
+    vertical-equiv-iso-natural to =
+      ∀ {x y x′ x″ y′} {f : Hom x y}
+      → (f′ : Hom[ f ] x″ y′) (g′ : Hom[ id ] x′ x″)
+      → to (hom[ idr _ ] (f′ ∘′ g′)) ≡[ sym (idl id) ] to f′ ∘′ g′
+
+  vertical-equiv→weak-fibration
+    : (to* : ∀ {x y x′ y′} {f : Hom x y} → Hom[ f ] x′ y′ → Hom[ id ] x′ (f *₀ y′))
+    → (∀ {x y x′ y′} {f : Hom x y} → is-equiv (to* {x} {y} {x′} {y′} {f}))
+    → vertical-equiv-iso-natural to*
+    → is-weak-cartesian-fibration
+  vertical-equiv→weak-fibration to* to-eqv natural .weak-lift f y′ = f-lift where
+```
+
+To start, we note that the inverse portion of the equivalence is also
+natural.
+
+```agda
+    from* : ∀ {x y x′ y′} {f : Hom x y} → Hom[ id ] x′ (f *₀ y′) → Hom[ f ] x′ y′
+    from* = equiv→inverse to-eqv
+
+    from*-natural
       : ∀ {x y} {f : Hom x y} {x′ x″ : Ob[ x ]} {y′ : Ob[ y ]}
-      → (f′ : Hom[ id ] x″ (U f .F₀ y′)) (g′ : Hom[ id ] x′ x″)
-      → from (hom[ idl id ] (f′ ∘′ g′)) ≡[ sym (idr f) ] from f′ ∘′ g′
-    from-natural {f = f} f′ g′ =
+      → (f′ : Hom[ id ] x″ (f *₀ y′)) (g′ : Hom[ id ] x′ x″)
+      → from* (hom[ idl id ] (f′ ∘′ g′)) ≡[ sym (idr f) ] from* f′ ∘′ g′
+    from*-natural {f = f} f′ g′ =
       to-pathp⁻ $ ap fst $ is-contr→is-prop (to-eqv .is-eqv (hom[ idl id ] (f′ ∘′ g′)))
-        (from (hom[ idl id ] (f′ ∘′ g′)) , equiv→counit to-eqv _)
-        (hom[ idr f ] (from f′ ∘′ g′) , from-pathp⁻ (natural (from f′) g′) ∙
+        (from* (hom[ idl id ] (f′ ∘′ g′)) , equiv→counit to-eqv _)
+        (hom[ idr f ] (from* f′ ∘′ g′) , from-pathp⁻ (natural (from* f′) g′) ∙
                                         (hom[]⟩⟨ ap (_∘′ g′) (equiv→counit to-eqv _)))
+```
+
+We then proceed to construct a weak lift of $f$. We can use our object
+lifting function to construct the domain of the lift, apply the inverse
+direction of the equivalence to $id' : f^{*}(y') \to f^{*}(y')$ to
+obtain the required lifting $x' \to_{f} f^{*}(y')$.
 
-    weak-lift : Weak-cartesian-lift f y′
-    weak-lift .x′ = U f .F₀ y′
-    weak-lift .lifting = from id′
-    weak-lift .weak-cartesian .universal g′ = to g′
-    weak-lift .weak-cartesian .commutes g′ = to-pathp $
-      hom[] (from id′ ∘′ to g′)   ≡˘⟨ from-pathp⁻ (from-natural id′ (to g′)) ⟩
-      from (hom[] (id′ ∘′ to g′)) ≡⟨ ap from idl[] ⟩
-      from (to g′)                ≡⟨ equiv→unit to-eqv g′ ⟩
-      g′ ∎
-    weak-lift .weak-cartesian .unique {g′ = g′} h′ p =
-      h′                          ≡˘⟨ idl[] {p = idl id} ⟩
-      hom[] (id′ ∘′ h′)           ≡˘⟨  hom[]⟩⟨ ap (_∘′ h′) (equiv→counit to-eqv id′) ⟩
-      hom[] (to (from id′) ∘′ h′) ≡˘⟨ from-pathp⁻ (natural (from id′) h′) ⟩
-      to (hom[] (from id′ ∘′ h′)) ≡⟨ ap to (from-pathp p) ⟩
-      to g′                       ∎
+```agda
+    f-lift : Weak-cartesian-lift f y′
+    f-lift .x′ = f *₀ y′
+    f-lift .lifting = from* id′
+```
+
+Now, we must show that the constructed lifting is weakly cartesian. We
+can use the forward direction of the equivalence to construct the
+universal map; the remaining properties follow from the fact that
+the equivalence is natural.
+
+```agda
+    f-lift .weak-cartesian .universal g′ = to* g′
+    f-lift .weak-cartesian .commutes g′ = to-pathp $
+      hom[] (from* id′ ∘′ to* g′)   ≡˘⟨ from-pathp⁻ (from*-natural id′ (to* g′)) ⟩
+      from* (hom[] (id′ ∘′ to* g′)) ≡⟨ ap from* idl[] ⟩
+      from* (to* g′)                ≡⟨ equiv→unit to-eqv g′ ⟩
+      g′                            ∎
+    f-lift .weak-cartesian .unique {g′ = g′} h′ p =
+      h′                            ≡˘⟨ idl[] {p = idl id} ⟩
+      hom[] (id′ ∘′ h′)             ≡˘⟨ hom[]⟩⟨ ap (_∘′ h′) (equiv→counit to-eqv id′) ⟩
+      hom[] (to* (from* id′) ∘′ h′) ≡˘⟨ from-pathp⁻ (natural (from* id′) h′) ⟩
+      to* (hom[] (from* id′ ∘′ h′)) ≡⟨ ap to* (from-pathp p) ⟩
+      to* g′                        ∎
+```
+
+<!--
+```agda
+module _ (U : ∀ {x y} → Hom x y → Functor (Fibre ℰ y) (Fibre ℰ x)) where
+  open Functor
+  open _=>_
+
+  hom-iso→weak-fibration
+    : (∀ {x y y′} (u : Hom x y)
+       → natural-iso (Hom-over-into ℰ u y′) (Hom-into (Fibre ℰ x) (U u .F₀ y′)))
+    → is-weak-cartesian-fibration
+  hom-iso→weak-fibration hom-iso =
+    vertical-equiv→weak-fibration
+      (λ u → U u .F₀)
+      (λ u′ → natural-iso.to (hom-iso _) .η _ u′)
+      (natural-iso-to-is-equiv (hom-iso _) _)
+      λ f′ g′ → to-pathp⁻ $
+        happly (natural-iso.to (hom-iso _) .is-natural _ _ g′) f′
+```
+-->
+
+
+Note that this result does *not* extend to fibrations; the equivalence
+of homs can only get us weak cartesian lifts. To make the final step
+to a fibration, we need to use other means.
+
+However, we do obtain a natural isomorphism between $\cE_{u}(x',-)$ and
+$cE_{y}(x',u^{*}(-))$.
+
+```agda
+module _ (fib : Cartesian-fibration) where
+  open Cartesian-fibration fib
+  open Indexing ℰ fib
+
+  fibration→hom-iso-from
+    : ∀ {x y x′} (u : Hom x y)
+    → natural-iso
+      (Hom-over-from ℰ u x′)
+      (Hom-from (Fibre ℰ x) x′ F∘ base-change u)
+  fibration→hom-iso-from {x} {y} {x′} u = to-natural-iso mi where
+    open make-natural-iso
+
+    mi : make-natural-iso
+          (Hom-over-from ℰ u x′)
+          (Hom-from (Fibre ℰ x) x′ F∘ base-change u)
+    mi .eta x u′ = has-lift.universalv u x u′
+    mi .inv x v′ = hom[ idr u ] (has-lift.lifting u x ∘′ v′)
+    mi .eta∘inv x = funext λ v′ →
+      sym $ has-lift.uniquev u _ _ (to-pathp refl)
+    mi .inv∘eta x = funext λ u′ →
+      from-pathp (has-lift.commutesv u _ _)
+    mi .natural _ _ v′ = funext λ u′ →
+      has-lift.unique u _ _ $ to-pathp $
+        smashr _ _
+        ·· revive₁ (pulll[] _ (has-lift.commutesv u _ _))
+        ·· smashl _ _
+        ·· weave _ (pullr (idr u)) _ (pullr[] _ (has-lift.commutesv u _ _))
+        ·· duplicate id-comm-sym _ (idl u)
+```
+
+<!--
+```agda
+  fibration→universal-is-equiv
+    : ∀ {x y x′ y′}
+    → (f : Hom x y)
+    → is-equiv (has-lift.universalv f y′ {x′})
+  fibration→universal-is-equiv f =
+    weak-fibration→universal-is-equiv (fibration→weak-fibration fib) f
+
+  fibration→vertical-equiv
+    : ∀ {x y x′ y′}
+    → (f : Hom x y)
+    → Hom[ f ] x′ y′ ≃ Hom[ id ] x′ (has-lift.x′ f y′)
+  fibration→vertical-equiv f =
+    weak-fibration→vertical-equiv (fibration→weak-fibration fib) f
+
+  fibration→hom-iso-into
+    : ∀ {x y y′} (u : Hom x y)
+    → natural-iso
+      (Hom-over-into ℰ u y′)
+      (Hom-into (Fibre ℰ x) (has-lift.x′ u y′))
+  fibration→hom-iso-into u =
+    weak-fibration→hom-iso-into (fibration→weak-fibration fib) u
 ```
 -->
+
+If we combine this with `weak-fibration→hom-iso-into`{.Agda}, we obtain
+a natural iso between $\cE_{u}(-,-)$ and $\cE_{id}(-,u^{*}(-))$.
+
+```agda
+  fibration→hom-iso
+    : ∀ {x y} (u : Hom x y)
+    → natural-iso (Hom-over ℰ u) (Hom[-,-] (Fibre ℰ x) F∘ (Id F× base-change u))
+  fibration→hom-iso {x = x} u = to-natural-iso mi where
+    open make-natural-iso
+    open _=>_
+
+    module into-iso {y′} = natural-iso (fibration→hom-iso-into {y′ = y′} u)
+    module from-iso {x′} = natural-iso (fibration→hom-iso-from {x′ = x′} u)
+
+    mi : make-natural-iso (Hom-over ℰ u) (Hom[-,-] (Fibre ℰ x) F∘ (Id F× base-change u))
+    mi .eta x u′ = has-lift.universalv u _ u′
+    mi .inv x v′ = hom[ idr u ] (has-lift.lifting u _ ∘′ v′)
+    mi .eta∘inv x = funext λ v′ →
+      sym $ has-lift.uniquev u _ _ (to-pathp refl)
+    mi .inv∘eta x = funext λ u′ →
+      from-pathp (has-lift.commutesv u _ _)
+    mi .natural _ _ (v₁′ , v₂′) = funext λ u′ →
+      sym (apr′ (happly (into-iso.to .is-natural _ _ v₁′) u′))
+      ·· sym (happly (from-iso.to .is-natural _ _ v₂′) (hom[ idr _ ] (u′ ∘′ v₁′)))
+      ·· ap (into-iso.to .η _) (smashr _ _ ∙ reindex _ _ )
+```
diff --git a/src/Cat/Displayed/Cocartesian.lagda.md b/src/Cat/Displayed/Cocartesian.lagda.md
index 1a66a1b11..8d07823a2 100644
--- a/src/Cat/Displayed/Cocartesian.lagda.md
+++ b/src/Cat/Displayed/Cocartesian.lagda.md
@@ -122,6 +122,42 @@ to a unique universal factorisation of $h'$ through a map $b' \to_{m} u'$
           → m′ ∘′ f′ ≡[ p ] h′ → m′ ≡[ q ] universal′ r h′
   uniquep p q r {h′ = h′} m′ s  =
     to-pathp⁻ (unique m′ (from-pathp⁻ s) ∙ from-pathp⁻ (universalp p q r h′))
+
+  uniquep₂ : ∀ {u u′} {m₁ m₂ : Hom b u} {k : Hom a u}
+          → (p : m₁ ∘ f ≡ k) (q : m₁ ≡ m₂) (r : m₂ ∘ f ≡ k)
+          → {h′ : Hom[ k ] a′ u′}
+          → (m₁′ : Hom[ m₁ ] b′ u′)
+          → (m₂′ : Hom[ m₂ ] b′ u′)
+          → m₁′ ∘′ f′ ≡[ p ] h′
+          → m₂′ ∘′ f′ ≡[ r ] h′
+          → m₁′ ≡[ q ] m₂′
+  uniquep₂ p q r {h′ = h′} m₁′ m₂′ α β = to-pathp⁻ $
+       unique m₁′ (from-pathp⁻ α)
+    ·· from-pathp⁻ (universalp p q r _)
+    ·· ap hom[] (sym (unique m₂′ (from-pathp⁻ β)))
+
+  universalv : ∀ {b″} (f″ : Hom[ f ] a′ b″) → Hom[ id ] b′ b″
+  universalv f″ = universal′ (idl _) f″
+
+  commutesv
+    : ∀ {x′} (g′ : Hom[ f ] a′ x′)
+    → universalv g′ ∘′ f′ ≡[ idl _ ] g′
+  commutesv = commutesp (idl _)
+
+  uniquev
+    : ∀ {x′} {g′ : Hom[ f ] a′ x′}
+    → (h′ : Hom[ id ] b′ x′)
+    → h′ ∘′ f′ ≡[ idl _ ] g′
+    → h′ ≡ universalv g′
+  uniquev h′ p = uniquep (idl _) refl (idl _) h′ p
+
+  uniquev₂
+    : ∀ {x′} {g′ : Hom[ f ] a′ x′}
+    → (h′ h″ : Hom[ id ] b′ x′)
+    → h′ ∘′ f′ ≡[ idl _ ] g′
+    → h″ ∘′ f′ ≡[ idl _ ] g′
+    → h′ ≡ h″
+  uniquev₂ h′ h″ p q = uniquep₂ (idl _) refl (idl _) h′ h″ p q
 ```
 -->
 
@@ -362,6 +398,18 @@ record Cocartesian-fibration : Type (o ⊔ ℓ ⊔ o′ ⊔ ℓ′) where
   module has-lift {x y} (f : Hom x y) (x′ : Ob[ x ]) =
     Cocartesian-lift (has-lift f x′)
 ```
+
+<!--
+
+```agda
+  rebase : ∀ {x y x′ x″} → (f : Hom x y)
+           → Hom[ id ] x′ x″
+           → Hom[ id ] (has-lift.y′ f x′) (has-lift.y′ f x″)
+  rebase f vert =
+    has-lift.universalv f _ (hom[ idr _ ] (has-lift.lifting f _ ∘′ vert))
+```
+-->
+
 As expected, opfibrations are dual to fibrations.
 ```agda
 op-fibration→opfibration : Cartesian-fibration (ℰ ^total-op) → Cocartesian-fibration
diff --git a/src/Cat/Displayed/Cocartesian/Indexing.lagda.md b/src/Cat/Displayed/Cocartesian/Indexing.lagda.md
new file mode 100644
index 000000000..555069ca9
--- /dev/null
+++ b/src/Cat/Displayed/Cocartesian/Indexing.lagda.md
@@ -0,0 +1,72 @@
+```agda
+open import Cat.Displayed.Base
+open import Cat.Displayed.Cocartesian
+open import Cat.Displayed.Fibre
+open import Cat.Instances.Functor
+open import Cat.Prelude
+
+import Cat.Displayed.Reasoning
+import Cat.Reasoning
+
+module Cat.Displayed.Cocartesian.Indexing
+  {o ℓ o′ ℓ′} {ℬ : Precategory o ℓ}
+  (ℰ : Displayed ℬ o′ ℓ′)
+  (opfibration : Cocartesian-fibration ℰ)
+  where
+```
+
+<!--
+```agda
+open Cat.Reasoning ℬ
+open Displayed ℰ
+open Cat.Displayed.Reasoning ℰ
+open Cocartesian-fibration opfibration
+open Functor
+```
+-->
+
+# Opreindexing for Cocartesian fibrations
+
+[Opfibrations] are dual to [fibrations], so they inherit the ability
+to [reindex along morphisms in the base]. However, this reindexing is
+*covariant* for opfibrations, whereas it is *contravariant* for
+fibrations.
+
+[Opfibrations]: Cat.Displayed.Cocartesian.html
+[fibrations]: Cat.Displayed.Cartesian.html
+[reindex along morphisms in the base] Cat.Displayed.Cartesian.Indexing.html
+
+This difference in variance gives opfibrations a distinct character.
+Reindexing in fibrations can be thought of a sort of restriction map.
+This can be seen clearly with [the canonical self-indexing], where the
+reindexing functors are given by [pullbacks]. On the other hand,
+opreindexing can be thought of as an extension map. We can again use the
+the canonical self-indexing as our example: opreindexing is given by
+postcomposition, which extends families over $X$ to families over $Y$ by
+adding in empty fibres.
+
+[the canonical self-indexing]: Cat.Displayed.Instances.Slice.html
+[pullbacks]: Cat.Diagram.Pullback.html
+
+```agda
+cobase-change : ∀ {x y} (f : Hom x y) → Functor (Fibre ℰ x) (Fibre ℰ y)
+cobase-change f .F₀ ob = has-lift.y′ f ob
+cobase-change f .F₁ vert = rebase f vert
+```
+
+<!--
+```agda
+cobase-change f .F-id =
+  sym $ has-lift.uniquev _ _ _ $ to-pathp $
+    idl[] ∙ (sym $ cancel _ _ (idr′ _))
+cobase-change f .F-∘ f′ g′ =
+  sym $ has-lift.uniquev _ _ _ $ to-pathp $
+    smashl _ _
+    ·· revive₁ (pullr[] _ (has-lift.commutesv _ _ _))
+    ·· smashr _ _
+    ·· revive₁ (pulll[] _ (has-lift.commutesv _ _ _))
+      ·· smashl _ _
+      ·· sym assoc[]
+      ·· sym (smashr _ _)
+```
+-->
diff --git a/src/Cat/Displayed/Cocartesian/Weak.lagda.md b/src/Cat/Displayed/Cocartesian/Weak.lagda.md
index c3529cc7e..1551a24ba 100644
--- a/src/Cat/Displayed/Cocartesian/Weak.lagda.md
+++ b/src/Cat/Displayed/Cocartesian/Weak.lagda.md
@@ -2,13 +2,20 @@
 open import Cat.Displayed.Base
 open import Cat.Displayed.Cartesian
 open import Cat.Displayed.Cartesian.Weak
+open import Cat.Displayed.Fibre
 open import Cat.Displayed.Total.Op
+open import Cat.Functor.Hom
+open import Cat.Functor.Hom.Displayed
+open import Cat.Instances.Functor
+open import Cat.Instances.Product
 open import Cat.Prelude
 
 import Cat.Displayed.Cocartesian as Cocart
+import Cat.Displayed.Cocartesian.Indexing as Indexing
 import Cat.Displayed.Morphism
 import Cat.Displayed.Morphism.Duality
 import Cat.Displayed.Reasoning
+import Cat.Reasoning as CR
 
 module Cat.Displayed.Cocartesian.Weak
   {o ℓ o′ ℓ′}
@@ -19,7 +26,7 @@ module Cat.Displayed.Cocartesian.Weak
 
 <!--
 ```agda
-open Precategory ℬ
+open CR ℬ
 open Displayed ℰ
 open Cocart ℰ
 open Cat.Displayed.Morphism ℰ
@@ -368,12 +375,12 @@ $m^{*}$ is cartesian, thus finishing the proof.
         open Morphisms m h′
 
         id* : Hom[ id ] y′ y*
-        id* = m*.universal′ (idr _) m′
+        id* = m*.universalv m′
 
         path : m* ∘′ hom[ idl _ ] (id* ∘′ f′) ≡ h′
         path =
           m* ∘′ hom[] (id* ∘′ f′) ≡⟨ whisker-r _ ⟩
-          hom[] (m* ∘′ id* ∘′ f′) ≡⟨ cancel _ (ap (m ∘_) (idl _)) (pulll′ (idr _) (m*.commutesp (idr _) m′)) ⟩
+          hom[] (m* ∘′ id* ∘′ f′) ≡⟨ cancel _ (ap (m ∘_) (idl _)) (pulll′ (idr _) (m*.commutesv m′)) ⟩
           m′ ∘′ f′                ≡⟨ p ⟩
           h′ ∎
 ```
@@ -397,6 +404,7 @@ record Weak-cocartesian-lift
   open is-weak-cocartesian weak-cocartesian public
 ```
 
+
 As expected, weak cocartesian lifts are dual to weak cartesian lifts.
 
 ```agda
@@ -434,22 +442,101 @@ weak-cocartesian-lift→weak-co-cartesian-lift wlift .Weak-cartesian-lift.weak-c
 </details>
 
 A displayed category with all weak cocartesian lifts is called a
-**preopfibered category**. A preopfibred category is opfibered when
-weak cocartesian morphisms are closed under composition. This follows
-via duality.
+**weak cocartesian fibration**, though we will often refer to them
+as **weak opfibrations** These are also sometimes called
+**preopfibred categories**, though we avoid this terminology, as it
+conflicts with the precategory/category distinction.
+
+```agda
+record is-weak-cocartesian-fibration : Type (o ⊔ ℓ ⊔ o′ ⊔ ℓ′) where
+  no-eta-equality
+  field
+    weak-lift : ∀ {x y} → (f : Hom x y) → (x′ : Ob[ x ]) → Weak-cocartesian-lift f x′
+
+  module weak-lift {x y} (f : Hom x y) (x′ : Ob[ x ]) =
+    Weak-cocartesian-lift (weak-lift f x′)
+```
+
+<!--
+```agda
+  rebase : ∀ {x y x′ x″} → (f : Hom x y)
+           → Hom[ id ] x′ x″
+           → Hom[ id ] (weak-lift.y′ f x′) (weak-lift.y′ f x″)
+  rebase f vert =
+    weak-lift.universal f _ (hom[ idr _ ] (weak-lift.lifting f _ ∘′ vert))
+```
+-->
+
+Weak opfibrations are dual to [weak fibrations].
+```agda
+weak-op-fibration→weak-opfibration
+  : is-weak-cartesian-fibration (ℰ ^total-op)
+  → is-weak-cocartesian-fibration
+
+weak-opfibration→weak-op-fibration
+  : is-weak-cocartesian-fibration
+  → is-weak-cartesian-fibration (ℰ ^total-op)
+```
 
+
+<details>
+<summary>As usual, we omit the duality proofs, as they are quite tedious.
+</summary>
+```agda
+weak-op-fibration→weak-opfibration wlift .is-weak-cocartesian-fibration.weak-lift f x′ =
+  weak-co-cartesian-lift→weak-cocartesian-lift $
+  is-weak-cartesian-fibration.weak-lift wlift f x′
+
+weak-opfibration→weak-op-fibration wlift .is-weak-cartesian-fibration.weak-lift f y′ =
+  weak-cocartesian-lift→weak-co-cartesian-lift $
+  is-weak-cocartesian-fibration.weak-lift wlift f y′
+```
+</details>
+
+Every opfibration is a weak opfibration.
+
+```agda
+cocartesian-lift→weak-cocartesian-lift
+  : ∀ {x y} {f : Hom x y} {x′ : Ob[ x ]}
+  → Cocartesian-lift f x′
+  → Weak-cocartesian-lift f x′
+
+opfibration→weak-opfibration
+  : Cocartesian-fibration
+  → is-weak-cocartesian-fibration
+```
+
+<!--
 ```agda
-weak-cocartesian-lifts→opfibration
-  : (lifts : ∀ {x y} → (f : Hom x y) → (x′ : Ob[ x ]) → Weak-cocartesian-lift f x′)
+cocartesian-lift→weak-cocartesian-lift cocart .Weak-cocartesian-lift.y′ =
+  Cocartesian-lift.y′ cocart
+cocartesian-lift→weak-cocartesian-lift cocart .Weak-cocartesian-lift.lifting =
+  Cocartesian-lift.lifting cocart
+cocartesian-lift→weak-cocartesian-lift cocart .Weak-cocartesian-lift.weak-cocartesian =
+  cocartesian→weak-cocartesian (Cocartesian-lift.cocartesian cocart)
+
+opfibration→weak-opfibration opfib .is-weak-cocartesian-fibration.weak-lift f x′ =
+  cocartesian-lift→weak-cocartesian-lift (Cocartesian-fibration.has-lift opfib f x′)
+```
+-->
+
+
+
+A weak opfibration is an opfibration when weak cocartesian morphisms are
+closed under composition. This follows via duality.
+
+```agda
+weak-opfibration→opfibration
+  : is-weak-cocartesian-fibration
   → (∀ {x y z x′ y′ z′} {f : Hom y z} {g : Hom x y}
      → {f′ : Hom[ f ] y′ z′} {g′ : Hom[ g ] x′ y′}
      → is-weak-cocartesian f f′ → is-weak-cocartesian g g′
      → is-weak-cocartesian (f ∘ g) (f′ ∘′ g′))
   → Cocartesian-fibration
-weak-cocartesian-lifts→opfibration wlifts weak-∘ =
+weak-opfibration→opfibration wopfib weak-∘ =
   op-fibration→opfibration $
-  weak-cartesian-lifts→fibration (ℰ ^total-op)
-  (λ f y′ → weak-cocartesian-lift→weak-co-cartesian-lift (wlifts f y′))
+  weak-fibration→fibration (ℰ ^total-op)
+  (weak-opfibration→weak-op-fibration wopfib)
   (λ f g →
     weak-cocartesian→weak-co-cartesian $
     weak-∘
@@ -462,14 +549,198 @@ cocartesian maps are closed under composition, thanks to
 `fibration+weak-cocartesian→cocartesian`{.Agda}.
 
 ```agda
-cartesian+weak-cocartesian-lifts→opfibration
+cartesian+weak-opfibration→opfibration
   : Cartesian-fibration ℰ
-  → (∀ {x y} → (f : Hom x y) → (x′ : Ob[ x ]) → Weak-cocartesian-lift f x′)
+  → is-weak-cocartesian-fibration
   → Cocartesian-fibration
-cartesian+weak-cocartesian-lifts→opfibration fib wlifts =
-  weak-cocartesian-lifts→opfibration wlifts λ f-weak g-weak →
+cartesian+weak-opfibration→opfibration fib wlifts =
+  weak-opfibration→opfibration wlifts λ f-weak g-weak →
     cocartesian→weak-cocartesian $
     cocartesian-∘
       (fibration+weak-cocartesian→cocartesian fib f-weak)
       (fibration+weak-cocartesian→cocartesian fib g-weak)
 ```
+
+# Weak Opfibrations and Equivalence of Hom Sets
+
+If $\cE$ is a weak opfibration, then the hom sets $x' \to_f y'$ and
+$f^{*}(x') \to_{id} y'$ are equivalent, where $f^{*}(x')$ is the codomain
+of the lift of $f$ along $y'$.
+
+```agda
+module _ (wopfib : is-weak-cocartesian-fibration) where
+  open is-weak-cocartesian-fibration wopfib
+
+  weak-opfibration→universal-is-equiv
+    : ∀ {x y y′ x′}
+    → (u : Hom x y)
+    → is-equiv (weak-lift.universal u x′ {y′})
+  weak-opfibration→universal-is-equiv {x′ = x′} u =
+    is-iso→is-equiv $
+    iso (λ u′ → hom[ idl u ] (u′ ∘′ weak-lift.lifting u x′))
+        (λ u′ → sym $ weak-lift.unique u x′ u′ (to-pathp refl))
+        (λ u′ → cancel _ _ (weak-lift.commutes u x′ u′))
+
+  weak-opfibration→vertical-equiv
+    : ∀ {x y x′ y′}
+    → (u : Hom x y)
+    → Hom[ u ] x′ y′ ≃ Hom[ id ] (weak-lift.y′ u x′) y′
+  weak-opfibration→vertical-equiv {x′ = x′} u =
+    weak-lift.universal u x′ , weak-opfibration→universal-is-equiv u
+```
+
+Furthermore, this equivalence is natural.
+
+```agda
+  weak-opfibration→hom-iso-from
+    : ∀ {x y x′} (u : Hom x y)
+    → natural-iso (Hom-over-from ℰ u x′) (Hom-from (Fibre ℰ y) (weak-lift.y′ u x′))
+  weak-opfibration→hom-iso-from {y = y} {x′ = x′} u = to-natural-iso mi where
+    open make-natural-iso
+
+    u*x′ : Ob[ y ]
+    u*x′ = weak-lift.y′ u x′
+
+    mi : make-natural-iso (Hom-over-from ℰ u x′) (Hom-from (Fibre ℰ y) u*x′)
+    mi .eta x u′ = weak-lift.universal u x′ u′
+    mi .inv x v′ = hom[ idl u ] (v′ ∘′ weak-lift.lifting u x′)
+    mi .eta∘inv _ = funext λ v′ →
+      sym $ weak-lift.unique u _ _ (to-pathp refl)
+    mi .inv∘eta _ = funext λ u′ →
+      from-pathp $ weak-lift.commutes u _ _ 
+    mi .natural _ _ v′ = funext λ u′ →
+      weak-lift.unique _ _ _ $ to-pathp $
+        smashl _ _
+      ∙ weave _ (ap (_∘ u) (idl id)) _ (pullr′ _ (weak-lift.commutes _ _ _))
+```
+
+As in the [weak cartesian case], the converse is also true: if there is
+a lifting of objects `Ob[ x ] → Ob[ y ]` for every morphism $f : x \to y$
+in $\cB$, along with a equivalence of homs as above, then $\cE$ is a weak
+opfibration.
+
+[weak cartesian case]: Cat.Displayed.Cartesian.Weak.html#weak-fibrations-and-equivalence-of-hom-sets
+
+```agda
+module _ (_*₀_ : ∀ {x y} → Hom x y → Ob[ x ] → Ob[ y ]) where
+
+  private
+    vertical-equiv-iso-natural
+      : (∀ {x y x′ y′} {f : Hom x y} → Hom[ f ] x′ y′ → Hom[ id ] (f *₀ x′) y′)
+      → Type _
+    vertical-equiv-iso-natural to =
+      ∀ {x y x′ y′ y″} {g : Hom x y}
+      → (f′ : Hom[ id ] y′ y″) (g′ : Hom[ g ] x′ y′)
+      → to (hom[ idl g ] (f′ ∘′ g′)) ≡[ sym (idl id) ] f′ ∘′ to g′
+
+  vertical-equiv→weak-opfibration
+    : (to : ∀ {x y x′ y′} {f : Hom x y} → Hom[ f ] x′ y′ → Hom[ id ] (f *₀ x′) y′)
+    → (eqv : ∀ {x y x′ y′} {f : Hom x y} → is-equiv (to {x} {y} {x′} {y′} {f}))
+    → (natural : vertical-equiv-iso-natural to)
+    → is-weak-cocartesian-fibration
+  vertical-equiv→weak-opfibration to to-eqv natural =
+    weak-op-fibration→weak-opfibration $
+    vertical-equiv→weak-fibration (ℰ ^total-op) _*₀_ to to-eqv λ f′ g′ →
+      to-pathp (reindex _ _ ∙ from-pathp (natural g′ f′))
+```
+
+<!--
+```agda
+module _ (U : ∀ {x y} → Hom x y → Functor (Fibre ℰ x) (Fibre ℰ y)) where
+  open Functor
+  open _=>_
+
+  hom-iso→weak-opfibration
+    : (∀ {x y x′} (u : Hom x y)
+       → natural-iso (Hom-over-from ℰ u x′) (Hom-from (Fibre ℰ y) (U u .F₀ x′)))
+    → is-weak-cocartesian-fibration
+  hom-iso→weak-opfibration hom-iso =
+    vertical-equiv→weak-opfibration
+      (λ u → U u .F₀)
+      (λ u′ → natural-iso.to (hom-iso _) .η _ u′)
+      (natural-iso-to-is-equiv (hom-iso _) _)
+      λ f′ g′ → to-pathp⁻ $
+        happly (natural-iso.to (hom-iso _) .is-natural _ _ f′) g′
+```
+-->
+
+<!--
+```agda
+module _ (opfib : Cocartesian-fibration) where
+  open Cocartesian-fibration opfib
+  open Indexing ℰ opfib
+
+  opfibration→hom-iso-from
+    : ∀ {x y x′} (u : Hom x y)
+    → natural-iso (Hom-over-from ℰ u x′) (Hom-from (Fibre ℰ y) (has-lift.y′ u x′))
+  opfibration→hom-iso-from u =
+    weak-opfibration→hom-iso-from (opfibration→weak-opfibration opfib) u
+
+  opfibration→hom-iso-into
+    : ∀ {x y y′} (u : Hom x y)
+    → natural-iso
+        (Hom-over-into ℰ u y′)
+        (Hom-into (Fibre ℰ y) y′ F∘ Functor.op (cobase-change u) )
+  opfibration→hom-iso-into {y = y} {y′ = y′} u = to-natural-iso mi where
+    open make-natural-iso
+
+    mi : make-natural-iso
+           (Hom-over-into ℰ u y′)
+           (Hom-into (Fibre ℰ y) y′ F∘ Functor.op (cobase-change u) )
+    mi .eta x u′ = has-lift.universalv u x u′
+    mi .inv x v′ = hom[ idl u ] (v′ ∘′ has-lift.lifting u _)
+    mi .eta∘inv x = funext λ v′ →
+      sym $ has-lift.uniquev u _ _ (to-pathp refl)
+    mi .inv∘eta x = funext λ u′ →
+      from-pathp (has-lift.commutesv u _ _)
+    mi .natural _ _ v′ = funext λ u′ →
+      has-lift.unique u _ _ $ to-pathp $
+        smashl _ _
+        ·· revive₁ (pullr[] _ (has-lift.commutesv u _ _))
+        ·· smashr _ _
+        ·· weave _ (pulll (idl u)) _ (pulll[] _ (has-lift.commutesv u _ _))
+        ·· duplicate id-comm _ (idr u)
+
+  opfibration→hom-iso
+    : ∀ {x y} (u : Hom x y)
+    → natural-iso
+        (Hom-over ℰ u)
+        (Hom[-,-] (Fibre ℰ y) F∘ (Functor.op (cobase-change u) F× Id))
+  opfibration→hom-iso {y = y} u = to-natural-iso mi where
+    open make-natural-iso
+    open _=>_
+    open Functor
+
+    module into-iso {y′} = natural-iso (opfibration→hom-iso-into {y′ = y′} u)
+    module from-iso {x′} = natural-iso (opfibration→hom-iso-from {x′ = x′} u)
+    module Fibre {x} = CR (Fibre ℰ x)
+
+    mi : make-natural-iso
+           (Hom-over ℰ u)
+           (Hom[-,-] (Fibre ℰ y) F∘ (Functor.op (cobase-change u) F× Id))
+    mi .eta x u′ = has-lift.universalv u _ u′
+    mi .inv x v′ = hom[ idl u ] (v′ ∘′ has-lift.lifting u _)
+    mi .eta∘inv x = funext λ v′ →
+      sym $ has-lift.uniquev u _ _ (to-pathp refl)
+    mi .inv∘eta x = funext λ u′ →
+      from-pathp (has-lift.commutesv u _ _)
+    mi .natural _ _ (v₁′ , v₂′) = funext λ u′ →
+      Fibre.pulll (sym (happly (from-iso.to .is-natural _ _ v₂′) u′))
+      ·· sym (happly (into-iso.to .is-natural _ _ v₁′) (hom[ idl _ ] (v₂′ ∘′ u′)))
+      ·· ap (into-iso.to .η _) (smashl _ _ ∙ sym assoc[])
+
+  opfibration→universal-is-equiv
+    : ∀ {x y x′ y′}
+    → (u : Hom x y)
+    → is-equiv (has-lift.universalv u y′ {x′})
+  opfibration→universal-is-equiv u =
+    weak-opfibration→universal-is-equiv (opfibration→weak-opfibration opfib) u
+
+  opfibration→vertical-equiv
+    : ∀ {x y x′ y′}
+    → (u : Hom x y)
+    → Hom[ u ] x′ y′ ≃ Hom[ id ] (has-lift.y′ u x′) y′
+  opfibration→vertical-equiv u =
+   weak-opfibration→vertical-equiv (opfibration→weak-opfibration opfib) u
+```
+-->
diff --git a/src/Cat/Displayed/Instances/Slice.lagda.md b/src/Cat/Displayed/Instances/Slice.lagda.md
index 33a31df41..36f53d5f4 100644
--- a/src/Cat/Displayed/Instances/Slice.lagda.md
+++ b/src/Cat/Displayed/Instances/Slice.lagda.md
@@ -1,5 +1,6 @@
 ```agda
 open import Cat.Displayed.Cartesian
+open import Cat.Displayed.Cocartesian
 open import Cat.Functor.Equivalence
 open import Cat.Diagram.Pullback
 open import Cat.Displayed.Fibre
@@ -235,3 +236,26 @@ reinterpret the above results as, essentially, giving the [pullback
 functors] between slice categories.
 
 [pullback functors]: Cat.Functor.Pullback.html
+
+## As an Opfibration
+
+The canonical self-indexing is *always* an opfibration, where
+opreindexing is given by postcomposition. If we think about slices as
+families, then opreindexing along $X \to Y$ extends a family over $X$
+to a family over $Y$ by adding in empty fibres for all elements of $Y$
+that do not lie in the image of $f$.
+
+```agda
+Codomain-opfibration : Cocartesian-fibration Slices
+Codomain-opfibration .Cocartesian-fibration.has-lift f x′ = lift-f where
+
+  lift-f : Cocartesian-lift Slices f x′
+  lift-f .Cocartesian-lift.y′ = cut (f ∘ x′ .map)
+  lift-f .Cocartesian-lift.lifting = slice-hom id (sym (idr _))
+  lift-f .Cocartesian-lift.cocartesian .is-cocartesian.universal m h′ =
+    slice-hom (h′ .to) (assoc _ _ _ ∙ h′ .commute)
+  lift-f .Cocartesian-lift.cocartesian .is-cocartesian.commutes m h′ =
+    Slice-pathp refl (idr _)
+  lift-f .Cocartesian-lift.cocartesian .is-cocartesian.unique m′ p =
+    Slice-pathp refl (sym (idr _) ∙ ap to p)
+```
diff --git a/src/Cat/Displayed/Instances/Trivial.lagda.md b/src/Cat/Displayed/Instances/Trivial.lagda.md
new file mode 100644
index 000000000..f841f2955
--- /dev/null
+++ b/src/Cat/Displayed/Instances/Trivial.lagda.md
@@ -0,0 +1,114 @@
+```agda
+open import Cat.Displayed.Base
+open import Cat.Displayed.Bifibration
+open import Cat.Displayed.Cartesian
+open import Cat.Displayed.Cocartesian
+open import Cat.Displayed.Fibre
+open import Cat.Displayed.Total
+open import Cat.Instances.Shape.Terminal
+open import Cat.Functor.Equivalence
+open import Cat.Functor.Equivalence.Path
+open import Cat.Prelude
+
+module Cat.Displayed.Instances.Trivial
+  {o ℓ} (𝒞 : Precategory o ℓ)
+  where
+```
+
+<!--
+```
+open Precategory 𝒞
+open Functor
+open Total-hom
+```
+-->
+
+# The Trivial Bifibration
+
+Any category $\ca{C}$ can be regarded as being displayed over the
+terminal category $\top$.
+
+```agda
+Trivial : Displayed ⊤Cat o ℓ 
+Trivial .Displayed.Ob[_] _ = Ob
+Trivial .Displayed.Hom[_] _ = Hom
+Trivial .Displayed.Hom[_]-set _ _ _ = Hom-set _ _
+Trivial .Displayed.id′ = id
+Trivial .Displayed._∘′_ = _∘_
+Trivial .Displayed.idr′ = idr
+Trivial .Displayed.idl′ = idl
+Trivial .Displayed.assoc′ = assoc
+```
+
+All morphisms in the trivial displayed category are vertical over the same object,
+so producing cartesian lifts is extremely easy: just use the identity
+morphism!
+
+```agda
+open Cartesian-fibration
+open Cocartesian-fibration
+open Cartesian-lift
+open Cocartesian-lift
+
+Trivial-fibration : Cartesian-fibration Trivial
+Trivial-fibration .has-lift f y′ .x′ = y′
+Trivial-fibration .has-lift f y′ .lifting = id
+Trivial-fibration .has-lift f y′ .cartesian = cartesian-id Trivial
+```
+
+We can use a similar line of argument to deduce that it is also an opfibration.
+
+```agda
+Trivial-opfibration : Cocartesian-fibration Trivial
+Trivial-opfibration .has-lift f x′ .y′ =
+  x′
+Trivial-opfibration .has-lift f x′ .lifting = id
+Trivial-opfibration .has-lift f x′ .cocartesian = cocartesian-id Trivial
+```
+
+Therefore, it is also a bifibration.
+
+```agda
+Trivial-bifibration : is-bifibration Trivial
+Trivial-bifibration .is-bifibration.fibration = Trivial-fibration
+Trivial-bifibration .is-bifibration.opfibration = Trivial-opfibration
+```
+
+Furthermore, the total category of the trivial bifibration is *isomorphic*
+to the category we started with.
+
+```agda
+trivial-total : Functor (∫ Trivial) 𝒞
+trivial-total .F₀ = snd
+trivial-total .F₁ = preserves
+trivial-total .F-id = refl
+trivial-total .F-∘ _ _ = refl
+
+trivial-total-iso : is-precat-iso trivial-total
+trivial-total-iso .is-precat-iso.has-is-ff =
+  is-iso→is-equiv $
+    iso (total-hom tt)
+        (λ _ → refl)
+        (λ _ → total-hom-pathp Trivial refl refl refl refl)
+trivial-total-iso .is-precat-iso.has-is-iso =
+  is-iso→is-equiv $
+    iso (tt ,_)
+        (λ _ → refl)
+        (λ _ → refl ,ₚ refl)
+```
+
+As the trivial bifibration only has one fibre, this fibre is also
+isomorphic to $\cE$.
+
+```agda
+trivial-fibre : Functor (Fibre Trivial tt) 𝒞
+trivial-fibre .F₀ x = x
+trivial-fibre .F₁ f = f
+trivial-fibre .F-id = refl
+trivial-fibre .F-∘ _ _ = transport-refl _
+
+trivial→fibre-iso : is-precat-iso trivial-fibre
+trivial→fibre-iso .is-precat-iso.has-is-ff = id-equiv
+trivial→fibre-iso .is-precat-iso.has-is-iso = id-equiv
+```
+
diff --git a/src/Cat/Displayed/Reasoning.lagda.md b/src/Cat/Displayed/Reasoning.lagda.md
index 49cc5dc3a..1e42abb04 100644
--- a/src/Cat/Displayed/Reasoning.lagda.md
+++ b/src/Cat/Displayed/Reasoning.lagda.md
@@ -79,6 +79,12 @@ hom[]-∙
       {f′ : E.Hom[ f ] x y}
   → hom[ q ] (hom[ p ] f′) ≡ hom[ p ∙ q ] f′
 hom[]-∙ p q = sym (subst-∙ (λ h → E.Hom[ h ] _ _) _ _ _)
+
+duplicate
+  : ∀ {a b x y} {f f' g : B.Hom a b} (p : f ≡ g) (q : f' ≡ g) (r : f ≡ f')
+      {f′ : E.Hom[ f ] x y}
+  → hom[ p ] f′ ≡ hom[ q ] (hom[ r ] f′)
+duplicate p q r = reindex _ _ ∙ sym (hom[]-∙ r q)
 ```
 
 To understand why these whiskering lemmas have such complicated types,
@@ -117,6 +123,24 @@ whisker-l {g = g} {a′} {_} {c′} {f′ = f′} {g′ = g′} p i =
     j (j = i0) → transport-filler (λ i → E.Hom[ p i B.∘ g ] _ _) (f′ E.∘′ g′) i
 ```
 
+<!--
+```agda
+unwhisker-r
+  : ∀ {a b c} {f : B.Hom b c} {g g' : B.Hom a b} {a′ b′ c′}
+      {f′ : E.Hom[ f ] b′ c′} {g′ : E.Hom[ g ] a′ b′}
+  → (p : f B.∘ g ≡ f B.∘ g') (q : g ≡ g')
+  → hom[ p ] (f′ E.∘′ g′) ≡ f′ E.∘′ hom[ q ] g′
+unwhisker-r p q = reindex _ _ ∙ sym (whisker-r _)
+
+unwhisker-l
+  : ∀ {a b c} {f f' : B.Hom b c} {g : B.Hom a b} {a′ b′ c′}
+      {f′ : E.Hom[ f ] b′ c′} {g′ : E.Hom[ g ] a′ b′}
+  → (p : f B.∘ g ≡ f' B.∘ g) (q : f ≡ f')
+  → hom[ p ] (f′ E.∘′ g′) ≡ hom[ q ] f′ E.∘′ g′
+unwhisker-l p q = reindex _ _ ∙ sym (whisker-l _)
+```
+-->
+
 The rest of this module is made up of grueling applications of the three
 lemmas above:
 
@@ -135,6 +159,20 @@ smashl
   → hom[ q ] (hom[ p ] f′ E.∘′ g′) ≡ hom[ ap (B._∘ g) p ∙ q ] (f′ E.∘′ g′)
 smashl p q = ap hom[ q ] (whisker-l p) ∙ hom[]-∙ _ _
 
+expandl
+  : ∀ {a b c} {f f' : B.Hom b c} {g : B.Hom a b} {h : B.Hom a c} {a′ b′ c′}
+      {f′ : E.Hom[ f ] b′ c′} {g′ : E.Hom[ g ] a′ b′}
+  → (p : f ≡ f') (q : f B.∘ g ≡ h)
+  → hom[ q ] (f′ E.∘′ g′) ≡ hom[ ap (B._∘ g) (sym p) ∙ q ] (hom[ p ] f′ E.∘′ g′)
+expandl p q = reindex q _ ∙ (sym $ smashl _ _)
+
+expandr
+  : ∀ {a b c} {f : B.Hom b c} {g g' : B.Hom a b} {h : B.Hom a c} {a′ b′ c′}
+      {f′ : E.Hom[ f ] b′ c′} {g′ : E.Hom[ g ] a′ b′}
+  → (p : g ≡ g') (q : f B.∘ g ≡ h)
+  → hom[ q ] (f′ E.∘′ g′) ≡ hom[ ap (f B.∘_) (sym p) ∙ q ] (f′ E.∘′ hom[ p ] g′)
+expandr p q = reindex q _ ∙ (sym $ smashr _ _)
+
 yank
   : ∀ {a b c d}
       {f : B.Hom c d} {g : B.Hom b c} {h : B.Hom a b} {i : B.Hom a c} {j : B.Hom b d}
@@ -404,14 +442,22 @@ module _ {a′ : Hom[ a ] y′ z′} {b′ : Hom[ b ] x′ y′} {c′ : Hom[ c
     hom[ refl ] (c′ ∘′ f′)                          ≡⟨ liberate _ ⟩
     c′ ∘′ f′                                        ∎
 
+  pulll[] : ∀ {f′ : Hom[ f ] w′ x′}
+           → a′ ∘′ (b′ ∘′ f′) ≡[ pulll p ] c′ ∘′ f′
+  pulll[] = pulll′
+
   pullr′ : ∀ {f′ : Hom[ f ] z′ w′} {q : (f ∘ a) ∘ b ≡ f ∘ c}
-           → (f′ ∘′ a′) ∘′ b′ ≡[ q ] f′ ∘′ c′
+         → (f′ ∘′ a′) ∘′ b′ ≡[ q ] f′ ∘′ c′
   pullr′ {f = f} {f′ = f′} {q = q} = to-pathp $
     hom[ q ] ((f′ ∘′ a′) ∘′ b′)             ≡˘⟨ assoc[] ⟩
     hom[ assoc f a b ∙ q ] (f′ ∘′ a′ ∘′ b′) ≡⟨ apr′ p′ ⟩
     hom[ refl ] (f′ ∘′ c′)                  ≡⟨ liberate _ ⟩
     f′ ∘′ c′                                ∎
 
+  pullr[] : ∀ {f′ : Hom[ f ] z′ w′}
+          → (f′ ∘′ a′) ∘′ b′ ≡[ pullr p ] f′ ∘′ c′
+  pullr[] = pullr′
+
 module _ {a′ : Hom[ a ] y′ z′} {b′ : Hom[ b ] x′ y′} {c′ : Hom[ c ] x′ z′}
          (p : c ≡ a ∘ b) (p′ : c′ ≡[ p ] a′ ∘′ b′) where abstract
 
@@ -420,11 +466,19 @@ module _ {a′ : Hom[ a ] y′ z′} {b′ : Hom[ b ] x′ y′} {c′ : Hom[ c
   pushl′ {f′ = f′} {q = q} i =
     pulll′ (sym p) (λ j → p′ (~ j)) {f′ = f′} {q = sym q} (~ i)
 
+  pushl[] : ∀ {f′ : Hom[ f ] w′ x′}
+           → c′ ∘′ f′ ≡[ pushl p ] a′ ∘′ (b′ ∘′ f′)
+  pushl[] = pushl′
+
   pushr′ : ∀ {f′ : Hom[ f ] z′ w′} {q : f ∘ c ≡ (f ∘ a) ∘ b}
            → f′ ∘′ c′ ≡[ q ] (f′ ∘′ a′) ∘′ b′
   pushr′ {f′ = f′} {q = q} i =
     pullr′ (sym p) (λ j → p′ (~ j)) {f′ = f′} {q = sym q} (~ i)
 
+  pushr[] : ∀ {f′ : Hom[ f ] z′ w′}
+           → f′ ∘′ c′ ≡[ pushr p ] (f′ ∘′ a′) ∘′ b′
+  pushr[] = pushr′
+
 module _ {f′ : Hom[ f ] y′ z′} {h′ : Hom[ h ] x′ y′}
          {g′ : Hom[ g ] y′ z′} {i′ : Hom[ i ] x′ y′}
          (p : f ∘ h ≡ g ∘ i) (p′ : f′ ∘′ h′ ≡[ p ] g′ ∘′ i′) where abstract
@@ -473,6 +527,10 @@ module _ {a′ : Hom[ a ] y′ x′} {b′ : Hom[ b ] x′ y′}
     hom[ sym (assoc a b f) ∙ q ] ((a′ ∘′ b′) ∘′ f′) ≡⟨ shiftl _ (eliml′ p p′) ⟩
     f′                                              ∎
 
+  cancell[] : ∀ {f′ : Hom[ f ] z′ x′}
+             → a′ ∘′ b′ ∘′ f′ ≡[ cancell p ] f′
+  cancell[] = cancell′
+
   cancelr′ : ∀ {f′ : Hom[ f ] x′ z′} {q : (f ∘ a) ∘ b ≡ f}
              → (f′ ∘′ a′) ∘′ b′ ≡[ q ] f′
   cancelr′ {f = f} {f′ = f′} {q = q} = to-pathp $
diff --git a/src/Cat/Displayed/Total/Op.lagda.md b/src/Cat/Displayed/Total/Op.lagda.md
index 67cab4e75..73c7b9058 100644
--- a/src/Cat/Displayed/Total/Op.lagda.md
+++ b/src/Cat/Displayed/Total/Op.lagda.md
@@ -1,5 +1,6 @@
 ```agda
 open import Cat.Displayed.Base
+open import Cat.Displayed.Fibre
 open import Cat.Displayed.Total
 open import Cat.Functor.Equivalence
 open import Cat.Functor.Equivalence.Path
@@ -7,6 +8,8 @@ open import Cat.Prelude
 
 open import 1Lab.Rewrite
 
+import Cat.Displayed.Reasoning as DR
+
 module Cat.Displayed.Total.Op where
 
 open Functor
@@ -18,7 +21,7 @@ open Total-hom
 Opposites of displayed categories are somewhat subtle, as there are
 multiple constructions that one could reasonably call the "opposite".
 The most obvious construction is to construct a new
-displayed category over $\ca{B}\op$; we call this category the
+displayed category over $\ca{B}op$; we call this category the
 **total opposite** of $\ca{E}$.
 
 ```agda
@@ -102,8 +105,6 @@ total-op→total-hom-is-equiv
 total-op→total-hom-is-equiv =
   is-iso→is-equiv $ iso total-hom→total-op (λ _ → refl) (λ _ → refl)
 
-
-
 total-op≡total-hom
   : ∀ {o ℓ o′ ℓ′} {ℬ : Precategory o ℓ} {ℰ : Displayed ℬ o′ ℓ′}
   → ∀ {x y} → Total-hom (ℰ ^total-op) x y ≡ Total-hom ℰ y x
@@ -140,3 +141,47 @@ Finally, we show that this extends to an equality of categories.
     (∫total-op→∫^op ℰ)
     (∫total-op≅∫^op ℰ)
 ```
+
+# Functors between fibres
+
+If there is a functor between the fibres of a displayed category $\cE$,
+then we also obtain a functor between the fibres of the total opposite
+of $\cE$.
+
+```agda
+fibre-functor-total-op
+  : ∀ {o ℓ o′ ℓ′} {ℬ : Precategory o ℓ} {ℰ : Displayed ℬ o′ ℓ′} {x y}
+  → Functor (Fibre ℰ x) (Fibre ℰ y)
+  → Functor (Fibre (ℰ ^total-op) x) (Fibre (ℰ ^total-op) y)
+fibre-functor-total-op F .F₀ = F .F₀
+fibre-functor-total-op F .F₁ = F .F₁
+fibre-functor-total-op F .F-id = F .F-id
+fibre-functor-total-op {ℰ = ℰ} F .F-∘ f g =
+  ap (F .F₁) (DR.reindex ℰ _ _ ) ·· F .F-∘ g f ·· DR.reindex ℰ _ _
+```
+
+<!--
+```agda
+fibre-functor-total-op-total-op  
+  : ∀ {o ℓ o′ ℓ′} {ℬ : Precategory o ℓ} {ℰ : Displayed ℬ o′ ℓ′} {x y}
+  → {F : Functor (Fibre ℰ x) (Fibre ℰ y)}
+  → fibre-functor-total-op (fibre-functor-total-op F) ≡ F
+fibre-functor-total-op-total-op {F = F} i .F₀ = F .F₀
+fibre-functor-total-op-total-op {F = F} i .F₁ = F .F₁
+fibre-functor-total-op-total-op  {F = F} i .F-id = F .F-id
+fibre-functor-total-op-total-op {ℰ = ℰ} {y = y} {F = F} i .F-∘ f g =
+  is-prop→pathp (λ i → Hom-set  _ _ _ (F .F₁ f ∘ F .F₁ g))
+    ((fibre-functor-total-op (fibre-functor-total-op F)) .F-∘ f g)
+    (F .F-∘ f g)
+    i
+    where open Precategory (Fibre ℰ y)
+
+private
+  fibre-functor-double-dual
+    : ∀ {o ℓ o′ ℓ′} {ℬ : Precategory o ℓ} {ℰ : Displayed ℬ o′ ℓ′} {x y}
+    → {F : Functor (Fibre ℰ x) (Fibre ℰ y)}
+    → fibre-functor-total-op (fibre-functor-total-op F) ≡rw F
+  fibre-functor-double-dual = make-rewrite fibre-functor-total-op-total-op
+{-# REWRITE fibre-functor-double-dual #-}
+```
+-->
diff --git a/src/Cat/Functor/Adjoint.lagda.md b/src/Cat/Functor/Adjoint.lagda.md
index 2a22bd1e4..0ea5bc3a0 100644
--- a/src/Cat/Functor/Adjoint.lagda.md
+++ b/src/Cat/Functor/Adjoint.lagda.md
@@ -574,6 +574,48 @@ $\hom(La,b) \cong \hom(a,Rb)$.
     (iso L-adjunct R-L-adjunct L-R-adjunct)
 ```
 
+Furthermore, these equivalences are natural.
+
+```agda
+  L-adjunct-naturall
+    : ∀ {a b c} (f : D.Hom (L.₀ b) c) (g : C.Hom a b)
+    → L-adjunct (f D.∘ L.₁ g) ≡ L-adjunct f C.∘ g
+  L-adjunct-naturall f g =
+    R.₁ (f D.∘ L.₁ g) C.∘ adj.unit.η _       ≡⟨ R.F-∘ _ _ C.⟩∘⟨refl ⟩
+    (R.₁ f C.∘ R.₁ (L.₁ g)) C.∘ adj.unit.η _ ≡⟨ C.extendr (sym $ adj.unit.is-natural _ _ _) ⟩
+    (R.₁ f C.∘ adj.unit.η _) C.∘ g           ∎
+
+  L-adjunct-naturalr 
+      : ∀ {a b c} (f : D.Hom b c) (g : D.Hom (L.₀ a) b)
+      → L-adjunct (f D.∘ g) ≡ R.₁ f C.∘ L-adjunct g
+  L-adjunct-naturalr f g = C.pushl (R.F-∘ f g)
+
+  L-adjunct-natural₂
+      : ∀ {a b c d} (f : D.Hom a b) (g : C.Hom c d) (x : D.Hom (L.F₀ d) a)
+      → L-adjunct (f D.∘ x D.∘ L.₁ g) ≡ R.₁ f C.∘ L-adjunct x C.∘ g
+  L-adjunct-natural₂ f g x =
+    L-adjunct-naturalr f (x D.∘ L.₁ g) ∙ ap (R.₁ f C.∘_) (L-adjunct-naturall x g)
+
+  R-adjunct-naturall
+      : ∀ {a b c} (f : C.Hom b (R.₀ c)) (g : C.Hom a b)
+      → R-adjunct (f C.∘ g) ≡ R-adjunct f D.∘ L.₁ g
+  R-adjunct-naturall f g = D.pushr (L.F-∘ f g)
+
+  R-adjunct-naturalr
+    : ∀ {a b c} (f : D.Hom b c) (g : C.Hom a (R.₀ b))
+    → R-adjunct (R.₁ f C.∘ g) ≡ f D.∘ R-adjunct g
+  R-adjunct-naturalr f g =
+    adj.counit.ε _ D.∘ L.₁ (R.₁ f C.∘ g)     ≡⟨ D.refl⟩∘⟨ L.F-∘ _ _ ⟩
+    adj.counit.ε _ D.∘ L.₁ (R.₁ f) D.∘ L.₁ g ≡⟨ D.extendl (adj.counit.is-natural _ _ _) ⟩
+    f D.∘ (adj.counit.ε _ D.∘ L.₁ g) ∎
+
+  R-adjunct-natural₂
+    : ∀ {a b c d} (f : D.Hom a b) (g : C.Hom c d) (x : C.Hom d (R.F₀ a))
+    → R-adjunct (R.₁ f C.∘ x C.∘ g) ≡ f D.∘ R-adjunct x D.∘ L.₁ g
+  R-adjunct-natural₂ f g x =
+    R-adjunct-naturalr f (x C.∘ g) ∙ ap (f D.∘_) (R-adjunct-naturall x g)
+```
+
 <!--
 ```agda
 module _ {L : Functor C D} {R : Functor D C} (adj : L ⊣ R) where
diff --git a/src/Cat/Functor/Adjoint/Hom.lagda.md b/src/Cat/Functor/Adjoint/Hom.lagda.md
index a22ccc9f4..d791bdfbd 100644
--- a/src/Cat/Functor/Adjoint/Hom.lagda.md
+++ b/src/Cat/Functor/Adjoint/Hom.lagda.md
@@ -6,26 +6,30 @@ description: |
 ---
 ```agda
 open import Cat.Functor.Adjoint
+open import Cat.Functor.Hom
+open import Cat.Instances.Functor
+open import Cat.Instances.Product
 open import Cat.Prelude
 
 import Cat.Functor.Reasoning as Func
 import Cat.Reasoning as Cat
 
-module Cat.Functor.Adjoint.Hom
-  {o ℓ o′ ℓ′} {C : Precategory o ℓ} {D : Precategory o′ ℓ′}
-  {L : Functor D C} {R : Functor C D}
-  where
+module Cat.Functor.Adjoint.Hom where
+
+module _ {o ℓ o′ ℓ′} {C : Precategory o ℓ} {D : Precategory o′ ℓ′}
+         {L : Functor D C} {R : Functor C D}
+         where
 ```
 
 <!--
 ```agda
-private
-  module C = Cat C
-  module D = Cat D
-  module L = Func L
-  module R = Func R
-open _⊣_
-open _=>_
+  private
+    module C = Cat C
+    module D = Cat D
+    module L = Func L
+    module R = Func R
+  open _⊣_
+  open _=>_
 ```
 -->
 
@@ -59,31 +63,31 @@ $\hom_\cD(-,R-)$ whose data has been "unfolded" into elementary
 terms.
 
 ```agda
-hom-iso-natural
-  : (∀ {x y} → C.Hom (L.₀ x) y → D.Hom x (R.₀ y))
-  → Type _
-hom-iso-natural f =
-  ∀ {a b c d} (g : C.Hom a b) (h : D.Hom c d) x
-  → f (g C.∘ x C.∘ L.₁ h) ≡ R.₁ g D.∘ f x D.∘ h
-
-hom-iso→adjoints
-  : (f : ∀ {x y} → C.Hom (L.₀ x) y → D.Hom x (R.₀ y))
-  → (eqv : ∀ {x y} → is-equiv (f {x} {y}))
-  → hom-iso-natural f
-  → L ⊣ R
-hom-iso→adjoints f f-equiv natural = adj′ where
-  f⁻¹ : ∀ {x y} → D.Hom x (R.₀ y) → C.Hom (L.₀ x) y
-  f⁻¹ = equiv→inverse f-equiv
-
-  inv-natural : ∀ {a b c d} (g : C.Hom a b) (h : D.Hom c d) x
-              → f⁻¹ (R.₁ g D.∘ x D.∘ h) ≡ g C.∘ f⁻¹ x C.∘ L.₁ h
-  inv-natural g h x = ap fst $ is-contr→is-prop (f-equiv .is-eqv _)
-    (f⁻¹ (R.₁ g D.∘ x D.∘ h) , refl)
-    ( g C.∘ f⁻¹ x C.∘ L.₁ h
-    , natural _ _ _
-    ∙ sym (equiv→counit f-equiv _)
-    ∙ ap (f ⊙ f⁻¹)
-         (D.extendl (ap (R.₁ g D.∘_) (equiv→counit f-equiv _))))
+  hom-iso-natural
+    : (∀ {x y} → C.Hom (L.₀ x) y → D.Hom x (R.₀ y))
+    → Type _
+  hom-iso-natural f =
+    ∀ {a b c d} (g : C.Hom a b) (h : D.Hom c d) x
+    → f (g C.∘ x C.∘ L.₁ h) ≡ R.₁ g D.∘ f x D.∘ h
+  
+  hom-iso→adjoints
+    : (f : ∀ {x y} → C.Hom (L.₀ x) y → D.Hom x (R.₀ y))
+    → (eqv : ∀ {x y} → is-equiv (f {x} {y}))
+    → hom-iso-natural f
+    → L ⊣ R
+  hom-iso→adjoints f f-equiv natural = adj′ where
+    f⁻¹ : ∀ {x y} → D.Hom x (R.₀ y) → C.Hom (L.₀ x) y
+    f⁻¹ = equiv→inverse f-equiv
+  
+    inv-natural : ∀ {a b c d} (g : C.Hom a b) (h : D.Hom c d) x
+                → f⁻¹ (R.₁ g D.∘ x D.∘ h) ≡ g C.∘ f⁻¹ x C.∘ L.₁ h
+    inv-natural g h x = ap fst $ is-contr→is-prop (f-equiv .is-eqv _)
+      (f⁻¹ (R.₁ g D.∘ x D.∘ h) , refl)
+      ( g C.∘ f⁻¹ x C.∘ L.₁ h
+      , natural _ _ _
+      ∙ sym (equiv→counit f-equiv _)
+      ∙ ap (f ⊙ f⁻¹)
+           (D.extendl (ap (R.₁ g D.∘_) (equiv→counit f-equiv _))))
 ```
 
 We do not require an explicit naturality witness for the inverse of $f$,
@@ -93,32 +97,103 @@ compute that $f(\id)$ and $f^{-1}(\id)$ do indeed give a system
 of adjunction units and co-units.
 
 ```agda
-  adj′ : L ⊣ R
-  adj′ .unit .η x = f C.id
-  adj′ .unit .is-natural x y h =
-    f C.id D.∘ h                    ≡⟨ D.introl R.F-id ⟩
-    R.₁ C.id D.∘ f C.id D.∘ h       ≡˘⟨ natural _ _ _ ⟩
-    f (C.id C.∘ C.id C.∘ L.₁ h)     ≡⟨ ap f (C.cancell (C.idl _) ∙ C.intror (C.idl _ ∙ L.F-id)) ⟩
-    f (L.₁ h C.∘ C.id C.∘ L.₁ D.id) ≡⟨ natural _ _ C.id ⟩
-    R.₁ (L.₁ h) D.∘ f C.id D.∘ D.id ≡⟨ D.refl⟩∘⟨ D.idr _ ⟩
-    R.₁ (L.₁ h) D.∘ f C.id          ∎
-  adj′ .counit .η x = f⁻¹ D.id
-  adj′ .counit .is-natural x y f =
-    f⁻¹ D.id C.∘ L.₁ (R.₁ f) ≡⟨ C.introl refl ⟩
-    C.id C.∘ f⁻¹ D.id C.∘ L.₁ (R.₁ f) ≡˘⟨ inv-natural _ _ _ ⟩
-    f⁻¹ (R.₁ C.id D.∘ D.id D.∘ R.₁ f) ≡⟨ ap f⁻¹ (D.cancell (D.idr _ ∙ R.F-id) ∙ D.intror (D.idl _)) ⟩
-    f⁻¹ (R.₁ f D.∘ D.id D.∘ D.id)     ≡⟨ inv-natural _ _ _ ⟩
-    f C.∘ f⁻¹ D.id C.∘ L.₁ D.id       ≡⟨ C.refl⟩∘⟨ C.elimr L.F-id ⟩
-    f C.∘ f⁻¹ D.id                    ∎
-  adj′ .zig =
-    f⁻¹ D.id C.∘ L.₁ (f C.id)          ≡⟨ C.introl refl ⟩
-    C.id C.∘ f⁻¹ D.id C.∘ L.₁ (f C.id) ≡˘⟨ inv-natural _ _ _ ⟩
-    f⁻¹ (R.₁ C.id D.∘ D.id D.∘ f C.id) ≡⟨ ap f⁻¹ (D.cancell (D.idr _ ∙ R.F-id)) ⟩
-    f⁻¹ (f C.id)                       ≡⟨ equiv→unit f-equiv _ ⟩
-    C.id                               ∎
-  adj′ .zag =
-    R.₁ (f⁻¹ D.id) D.∘ f C.id          ≡⟨ D.refl⟩∘⟨ D.intror refl ⟩
-    R.₁ (f⁻¹ D.id) D.∘ f C.id D.∘ D.id ≡˘⟨ natural _ _ _ ⟩
-    f (f⁻¹ D.id C.∘ C.id C.∘ L.₁ D.id) ≡⟨ ap f (C.elimr (C.idl _ ∙ L.F-id)) ⟩
-    f (f⁻¹ D.id)                       ≡⟨ equiv→counit f-equiv _ ⟩
-    D.id                               ∎
+    adj′ : L ⊣ R
+    adj′ .unit .η x = f C.id
+    adj′ .unit .is-natural x y h =
+      f C.id D.∘ h                    ≡⟨ D.introl R.F-id ⟩
+      R.₁ C.id D.∘ f C.id D.∘ h       ≡˘⟨ natural _ _ _ ⟩
+      f (C.id C.∘ C.id C.∘ L.₁ h)     ≡⟨ ap f (C.cancell (C.idl _) ∙ C.intror (C.idl _ ∙ L.F-id)) ⟩
+      f (L.₁ h C.∘ C.id C.∘ L.₁ D.id) ≡⟨ natural _ _ C.id ⟩
+      R.₁ (L.₁ h) D.∘ f C.id D.∘ D.id ≡⟨ D.refl⟩∘⟨ D.idr _ ⟩
+      R.₁ (L.₁ h) D.∘ f C.id          ∎
+    adj′ .counit .η x = f⁻¹ D.id
+    adj′ .counit .is-natural x y f =
+      f⁻¹ D.id C.∘ L.₁ (R.₁ f) ≡⟨ C.introl refl ⟩
+      C.id C.∘ f⁻¹ D.id C.∘ L.₁ (R.₁ f) ≡˘⟨ inv-natural _ _ _ ⟩
+      f⁻¹ (R.₁ C.id D.∘ D.id D.∘ R.₁ f) ≡⟨ ap f⁻¹ (D.cancell (D.idr _ ∙ R.F-id) ∙ D.intror (D.idl _)) ⟩
+      f⁻¹ (R.₁ f D.∘ D.id D.∘ D.id)     ≡⟨ inv-natural _ _ _ ⟩
+      f C.∘ f⁻¹ D.id C.∘ L.₁ D.id       ≡⟨ C.refl⟩∘⟨ C.elimr L.F-id ⟩
+      f C.∘ f⁻¹ D.id                    ∎
+    adj′ .zig =
+      f⁻¹ D.id C.∘ L.₁ (f C.id)          ≡⟨ C.introl refl ⟩
+      C.id C.∘ f⁻¹ D.id C.∘ L.₁ (f C.id) ≡˘⟨ inv-natural _ _ _ ⟩
+      f⁻¹ (R.₁ C.id D.∘ D.id D.∘ f C.id) ≡⟨ ap f⁻¹ (D.cancell (D.idr _ ∙ R.F-id)) ⟩
+      f⁻¹ (f C.id)                       ≡⟨ equiv→unit f-equiv _ ⟩
+      C.id                               ∎
+    adj′ .zag =
+      R.₁ (f⁻¹ D.id) D.∘ f C.id          ≡⟨ D.refl⟩∘⟨ D.intror refl ⟩
+      R.₁ (f⁻¹ D.id) D.∘ f C.id D.∘ D.id ≡˘⟨ natural _ _ _ ⟩
+      f (f⁻¹ D.id C.∘ C.id C.∘ L.₁ D.id) ≡⟨ ap f (C.elimr (C.idl _ ∙ L.F-id)) ⟩
+      f (f⁻¹ D.id)                       ≡⟨ equiv→counit f-equiv _ ⟩
+      D.id                               ∎
+```
+
+<!--
+```agda
+module _ {o ℓ o′} {C : Precategory o ℓ} {D : Precategory o′ ℓ}
+         {L : Functor D C} {R : Functor C D}
+         where
+  private
+    module C = Cat C
+    module D = Cat D
+    module L = Func L
+    module R = Func R
+
+
+  hom-natural-iso→adjoints
+    : natural-iso (Hom[-,-] C F∘ (Functor.op L F× Id)) (Hom[-,-] D F∘ (Id F× R))
+    → L ⊣ R
+  hom-natural-iso→adjoints eta =
+    hom-iso→adjoints (to .η _) (natural-iso-to-is-equiv eta (_ , _)) λ g h x →
+      happly (to .is-natural _ _ (h , g)) x
+    where
+      open natural-iso eta
+      open _=>_
+
+module _ {o ℓ o′} {C : Precategory o ℓ} {D : Precategory o′ ℓ}
+         {L : Functor D C} {R : Functor C D}
+         (adj : L ⊣ R)
+         where
+  private
+    module C = Cat C
+    module D = Cat D
+    module L = Func L
+    module R = Func R
+
+  adjunct-hom-iso-from
+    : ∀ a → natural-iso (Hom-from C (L.₀ a)) (Hom-from D a F∘ R)
+  adjunct-hom-iso-from a = to-natural-iso mi where
+    open make-natural-iso
+
+    mi : make-natural-iso (Hom-from C (L.₀ a)) (Hom-from D a F∘ R)
+    mi .eta x = L-adjunct adj
+    mi .inv x = R-adjunct adj
+    mi .eta∘inv _ = funext λ _ → L-R-adjunct adj _
+    mi .inv∘eta _ = funext λ _ → R-L-adjunct adj _
+    mi .natural _ _ f = funext λ g → sym (L-adjunct-naturalr adj f g)
+
+  adjunct-hom-iso-into
+    : ∀ b → natural-iso (Hom-into C b F∘ Functor.op L) (Hom-into D (R.₀ b))
+  adjunct-hom-iso-into b = to-natural-iso mi where
+    open make-natural-iso
+
+    mi : make-natural-iso (Hom-into C b F∘ Functor.op L) (Hom-into D (R.₀ b))
+    mi .eta x = L-adjunct adj
+    mi .inv x = R-adjunct adj
+    mi .eta∘inv _ = funext λ _ → L-R-adjunct adj _
+    mi .inv∘eta _ = funext λ _ → R-L-adjunct adj _
+    mi .natural _ _ f = funext λ g → sym $ L-adjunct-naturall adj g f
+
+  adjunct-hom-iso
+    : natural-iso (Hom[-,-] C F∘ (Functor.op L F× Id)) (Hom[-,-] D F∘ (Id F× R))
+  adjunct-hom-iso = to-natural-iso mi where
+    open make-natural-iso
+
+    mi : make-natural-iso (Hom[-,-] C F∘ (Functor.op L F× Id)) (Hom[-,-] D F∘ (Id F× R))
+    mi .eta x = L-adjunct adj
+    mi .inv x = R-adjunct adj
+    mi .eta∘inv _ = funext λ _ → L-R-adjunct adj _
+    mi .inv∘eta _ = funext λ _ → R-L-adjunct adj _
+    mi .natural _ _ (f , h) = funext λ g → sym $ L-adjunct-natural₂ adj h f g
+```
+-->
diff --git a/src/Cat/Functor/Hom.lagda.md b/src/Cat/Functor/Hom.lagda.md
index 62b699314..1eac6bb12 100644
--- a/src/Cat/Functor/Hom.lagda.md
+++ b/src/Cat/Functor/Hom.lagda.md
@@ -49,7 +49,6 @@ Hom[ x ,-] .F-id = funext (λ f → idl f)
 Hom[ x ,-] .F-∘ f g = funext λ h → sym (assoc f g h)
 ```
 
-
 ## The Yoneda embedding
 
 Abstractly and nonsensically, one could say that the Yoneda embedding
@@ -90,6 +89,17 @@ Hom[-,_] : Ob → Functor (C ^op) (Sets h)
 Hom[-,_] x = よ₀ x
 ```
 
+<!--
+```agda
+Hom-from : Ob → Functor C (Sets h)
+Hom-from = Hom[_,-]
+
+Hom-into : Ob → Functor (C ^op) (Sets h)
+Hom-into = よ₀
+```
+-->
+
+
 The morphism part takes a map $f$ to the transformation given by
 postcomposition; This is natural because we must show $f \circ x \circ g
 = (f \circ x) \circ g$, which is given by associativity in $C$.
diff --git a/src/Cat/Functor/Hom/Displayed.lagda.md b/src/Cat/Functor/Hom/Displayed.lagda.md
new file mode 100644
index 000000000..ec2029d50
--- /dev/null
+++ b/src/Cat/Functor/Hom/Displayed.lagda.md
@@ -0,0 +1,64 @@
+```agda
+open import Cat.Displayed.Base
+open import Cat.Displayed.Fibre
+open import Cat.Displayed.Total
+open import Cat.Displayed.Solver
+open import Cat.Instances.Product
+open import Cat.Prelude
+
+import Cat.Displayed.Reasoning
+
+module Cat.Functor.Hom.Displayed
+  {o ℓ o′ ℓ′} {ℬ : Precategory o ℓ} (ℰ : Displayed ℬ o′ ℓ′)
+  where
+```
+
+<!--
+```agda
+open Precategory ℬ
+open Displayed ℰ
+open Cat.Displayed.Reasoning ℰ
+open Functor
+```
+-->
+
+# Displayed Hom Functors
+
+Let $\cE$ be a displayed category over $\cB$. For every $u : x \to y$
+in the base, we can obtain a bifunctor from $\cE_{x}\op \times \cE_{y}$
+to $\Sets$, where $\cE_{x}$ denotes the [fibre category] of $\cE$ at $x$.
+The action of $(f, h)$ on $g$ is given by $h \circ g \circ f$, just as
+in the [non-displayed case].
+
+[bifunctor]: Cat.Functor.Bifunctor.html
+[fibre category]: Cat.Displayed.Fibre.html
+[non-displayed case]: Cat.Functor.Hom.html
+
+```agda
+Hom-over : ∀ {x y} → Hom x y → Functor (Fibre ℰ x ^op ×ᶜ Fibre ℰ y) (Sets ℓ′)
+Hom-over u .F₀ (a , b) = el (Hom[ u ] a b) (Hom[ u ]-set a b)
+Hom-over u .F₁ (f , h) g = hom[ idl _ ∙ idr _ ] (h ∘′ g ∘′ f)
+Hom-over u .F-id = funext λ f →
+  apr′ {q = idl _} (idr′ f) ∙ idl[]
+Hom-over u .F-∘ (f , h) (f' , h') = funext λ g →
+  hom[] (hom[] (h ∘′ h') ∘′ g ∘′ hom[] (f' ∘′ f)) ≡⟨ disp! ℰ ⟩
+  hom[] (h ∘′ hom[] (h' ∘′ g ∘′ f') ∘′ f) ∎
+```
+
+We can also define partially applied versions of this functor.
+
+```agda
+Hom-over-from : ∀ {x y} → Hom x y → Ob[ x ] → Functor (Fibre ℰ y) (Sets ℓ′)
+Hom-over-from u x′ .F₀ y′ = el (Hom[ u ] x′ y′) (Hom[ u ]-set x′ y′)
+Hom-over-from u x′ .F₁ f g = hom[ idl u ] (f ∘′ g)
+Hom-over-from u x′ .F-id = funext λ f → idl[]
+Hom-over-from u x′ .F-∘ f g  = funext λ h →
+  smashl _ _ ∙ sym assoc[] ∙ sym (smashr _ _)
+
+Hom-over-into : ∀ {x y} → Hom x y → Ob[ y ] → Functor (Fibre ℰ x ^op) (Sets ℓ′)
+Hom-over-into u y′ .F₀ x′ = el (Hom[ u ] x′ y′) (Hom[ u ]-set x′ y′)
+Hom-over-into u y′ .F₁ f g = hom[ idr u ] (g ∘′ f)
+Hom-over-into u y′ .F-id = funext λ f → idr[]
+Hom-over-into u y′ .F-∘ f g = funext λ h →
+  smashr _ _ ∙ assoc[] ∙ (sym $ smashl _ _ )
+```
diff --git a/src/Cat/Instances/Functor.lagda.md b/src/Cat/Instances/Functor.lagda.md
index b3e04765e..d9c6d29b2 100644
--- a/src/Cat/Instances/Functor.lagda.md
+++ b/src/Cat/Instances/Functor.lagda.md
@@ -37,27 +37,35 @@ $\eta$ and $\theta$.
 
 ```agda
 _∘nt_ : {F G H : Functor C D} → G => H → F => G → F => H
-_∘nt_ {C = C} {D = D} {F} {G} {H} f g = nat where
-  module D = Cat.Reasoning D
+_∘nt_ {C = C} {D = D} {F} {G} {H} f g = nat
+  module ∘nt where
+    module D = Cat.Reasoning D
 
-  nat : F => H
-  nat .η x = f .η _ D.∘ g .η _
+    nat : F => H
+    nat .η x = f .η _ D.∘ g .η _
 ```
 
 <!--
 ```agda
-  nat .is-natural x y h =
-    (f .η y D.∘ g .η y) D.∘ F.₁ h  ≡⟨ D.pullr (g .is-natural _ _ _) ⟩
-    f .η y D.∘ (G.₁ h D.∘ g .η x)  ≡⟨ D.extendl (f .is-natural _ _ _) ⟩
-    H.₁ h  D.∘ f .η _ D.∘ g .η  _  ∎
-    where
-      module C = Precategory C
-      module F = Functor F
-      module G = Functor G
-      module H = Functor H
+    nat .is-natural x y h =
+      (f .η y D.∘ g .η y) D.∘ F.₁ h  ≡⟨ D.pullr (g .is-natural _ _ _) ⟩
+      f .η y D.∘ (G.₁ h D.∘ g .η x)  ≡⟨ D.extendl (f .is-natural _ _ _) ⟩
+      H.₁ h  D.∘ f .η _ D.∘ g .η  _  ∎
+      where
+        module C = Precategory C
+        module F = Functor F
+        module G = Functor G
+        module H = Functor H
+```
+-->
+
+<!--
+```agda
+{-# DISPLAY ∘nt.nat f g = f ∘nt g #-}  
 ```
 -->
 
+
 We can then show that these definitions assemble into a category where
 the objects are functors $F, G : C \to D$, and the morphisms are natural
 transformations $F \To G$. This is because natural
@@ -434,6 +442,19 @@ module
     module D = Cat.Reasoning D
     module C = Cat.Reasoning C
 
+  natural-iso : (F G : Functor C D) → Type _
+  natural-iso F G = F CD.≅ G
+
+  module natural-iso {F G : Functor C D} (eta : F CD.≅ G) = CD._≅_ eta
+
+  _ni∘_ : ∀ {F G H : Functor C D}
+          → natural-iso F G → natural-iso G H
+          → natural-iso F H
+  _ni∘_ = CD._∘Iso_
+
+  _ni⁻¹ : ∀ {F G : Functor C D} → natural-iso F G → natural-iso G F
+  _ni⁻¹ = CD._Iso⁻¹
+
   F∘-iso-id-l
     : {F : Functor D D} {G : Functor C D}
     → F DD.≅ Id → (F F∘ G) CD.≅ G
@@ -509,5 +530,37 @@ module _
         (λ i j → G .F₀ (cd.iso→path-id {A = G′} i j .F₀ x))
         ∙ transport-refl _ ∙ sym (G .F-id)
     where module cd = Univalent cdcat
+
+module _ {o ℓ κ} {C : Precategory o ℓ} where
+  open Functor
+  open _=>_
+
+  natural-iso-to-is-equiv
+    : {F G : Functor C (Sets κ)}
+    → (eta : natural-iso F G)
+    → ∀ x → is-equiv (natural-iso.to eta .η x)
+  natural-iso-to-is-equiv eta x =
+    is-iso→is-equiv $
+      iso (natural-iso.from eta .η x)
+          (λ x i → natural-iso.invl eta i .η _ x)
+          (λ x i → natural-iso.invr eta i .η _ x)
+
+  natural-iso-from-is-equiv
+    : {F G : Functor C (Sets κ)}
+    → (eta : natural-iso F G)
+    → ∀ x → is-equiv (natural-iso.from eta .η x)
+  natural-iso-from-is-equiv eta x =
+    is-iso→is-equiv $
+      iso (natural-iso.to eta .η x)
+          (λ x i → natural-iso.invr eta i .η _ x)
+          (λ x i → natural-iso.invl eta i .η _ x)
+
+  natural-iso→equiv
+    : {F G : Functor C (Sets κ)}
+    → (eta : natural-iso F G)
+    → ∀ x → ∣ F .F₀ x ∣ ≃ ∣ G .F₀ x ∣
+  natural-iso→equiv eta x =
+    natural-iso.to eta .η x ,
+    natural-iso-to-is-equiv eta x
 ```
 -->
diff --git a/src/Cat/Instances/Product.lagda.md b/src/Cat/Instances/Product.lagda.md
index 6676ea7f5..c7ef5680e 100644
--- a/src/Cat/Instances/Product.lagda.md
+++ b/src/Cat/Instances/Product.lagda.md
@@ -14,7 +14,7 @@ open Precategory
 open Functor
 private variable
   o₁ h₁ o₂ h₂ : Level
-  C D E : Precategory o₁ h₁
+  B C D E : Precategory o₁ h₁
 ```
 -->
 
@@ -101,7 +101,24 @@ Cat⟨ F , G ⟩ = f where
   f .F₁ f = F₁ F f , F₁ G f
   f .F-id i = F-id F i , F-id G i
   f .F-∘ f g i = F-∘ F f g i , F-∘ G f g i
+
+_F×_ : Functor B D → Functor C E → Functor (B ×ᶜ C) (D ×ᶜ E)
+_F×_ {B = B} {D = D} {C = C} {E = E} G H = func
+  module F× where
+
+  func : Functor (B ×ᶜ C) (D ×ᶜ E)
+  func .F₀ (x , y) = (G .F₀ x) , (H .F₀ y)
+  func .F₁ (f , g) = (G .F₁ f) , (H .F₁ g)
+  func .F-id = (G .F-id) ,ₚ (H .F-id)
+  func .F-∘ (f , g) (f' , g') = (G .F-∘ f f') ,ₚ H .F-∘ g g'
+```
+
+<!--
+```agda
+{-# DISPLAY F×.func F G = F F× G #-}  
 ```
+-->
+
 
 ## Univalence
 
diff --git a/src/index.lagda.md b/src/index.lagda.md
index 86dda469f..9c1d25bc5 100644
--- a/src/index.lagda.md
+++ b/src/index.lagda.md
@@ -446,6 +446,9 @@ lemma:
 open import Cat.Functor.Hom -- Hom functor, Yoneda embedding, Coyoneda lemma
 open import Cat.Functor.Hom.Cocompletion -- Universal property of PSh(C)
 open import Cat.Functor.Hom.Representable -- Representable functors
+
+open import Cat.Functor.Hom.Displayed
+  -- Hom functors of displayed categories
 ```
 
 ## Univalent categories
@@ -667,6 +670,8 @@ open import Cat.Displayed.Instances.Scone
 -- We can consider *scones* over a category C with a terminal object as
 -- forming a displayed category over C. Moreover, it's a Cartesian
 -- fibration by construction.
+open import Cat.Displayed.Instances.Trivial
+-- Any category can be displayed over the terminal category.
 ```
 
 ### Cocartesian fibrations
@@ -675,10 +680,21 @@ open import Cat.Displayed.Instances.Scone
 open import Cat.Displayed.Cocartesian
   -- Cocartesian lifts, opfibrations
 
+open import Cat.Displayed.Cocartesian.Indexing
+  -- Opfibrations have covariant opreindexing 
+
 open import Cat.Displayed.Cocartesian.Weak
   -- Weak cocartesian morphisms
 ```
 
+### Bifibrations
+
+```agda
+open import Cat.Displayed.Bifibration
+  -- Bifibrations, adjoints to base change
+```
+
+
 
 ## Bicategories