diff --git a/Mathlib/CategoryTheory/Bicategory/Extension.lean b/Mathlib/CategoryTheory/Bicategory/Extension.lean
index 7efdf3ee502023..e189d39861e171 100644
--- a/Mathlib/CategoryTheory/Bicategory/Extension.lean
+++ b/Mathlib/CategoryTheory/Bicategory/Extension.lean
@@ -158,6 +158,37 @@ set_option backward.defeqAttrib.useBackward true in
 def whiskerOfCompIdIsoSelf (t : LeftExtension f g) : (t.whisker (𝟙 c)).ofCompId ≅ t :=
   StructuredArrow.isoMk (ρ_ (t.extension))
 
+section OfIso
+
+variable {f f' : a ⟶ b} (ef : f ≅ f') {g g' : a ⟶ c} (eg : g ≅ g')
+
+/-- Given isomorphisms `ef : f ≅ f'` and `eg : g ≅ g'`, the induced equivalence between their
+categories of left extensions. -/
+def mapIso : LeftExtension f g ≌ LeftExtension f' g' :=
+  (StructuredArrow.mapNatIso ((precomposing a b c).mapIso ef)).trans (StructuredArrow.mapIso eg)
+
+/-- Given isomorphisms `ef : f ≅ f'` and `eg : g ≅ g'`, and a left extension
+`t : LeftExtension f g`, the induced left extension `t.ofIso : LeftExtension f' g'`. -/
+def ofIso (t : LeftExtension f g) : LeftExtension f' g' :=
+  (mapIso ef eg).functor.obj t
+
+@[simp]
+theorem ofIso_extension (t : LeftExtension f g) :
+    (t.ofIso ef eg).extension = t.extension :=
+  rfl
+
+@[simp]
+theorem ofIso_unit (t : LeftExtension f g) :
+    (t.ofIso ef eg).unit = eg.inv ≫ t.unit ≫ ef.hom ▷ t.extension :=
+  rfl
+
+/-- Whiskering commutes with `LeftExtension.ofIso`. -/
+def whiskerOfIso (t : LeftExtension f g) {x : B} (h : c ⟶ x) :
+    (t.whisker h).ofIso ef (whiskerRightIso eg h) ≅ (t.ofIso ef eg).whisker h :=
+  StructuredArrow.isoMk (Iso.refl _) <| by simp [precomp]
+
+end OfIso
+
 end LeftExtension
 
 /-- Triangle diagrams for (left) lifts.
@@ -281,6 +312,37 @@ set_option backward.defeqAttrib.useBackward true in
 def whiskerOfIdCompIsoSelf (t : LeftLift f g) : (t.whisker (𝟙 c)).ofIdComp ≅ t :=
   StructuredArrow.isoMk (λ_ (lift t))
 
+section OfIso
+
+variable {f f' : b ⟶ a} (ef : f ≅ f') {g g' : c ⟶ a} (eg : g ≅ g')
+
+/-- Given isomorphisms `ef : f ≅ f'` and `eg : g ≅ g'`, the induced equivalence between their
+categories of left lifts. -/
+def mapIso : LeftLift f g ≌ LeftLift f' g' :=
+  (StructuredArrow.mapNatIso ((postcomposing c b a).mapIso ef)).trans (StructuredArrow.mapIso eg)
+
+/-- Given isomorphisms `ef : f ≅ f'` and `eg : g ≅ g'`, and a left lift `t : LeftLift f g`, the
+induced left lift `t.ofIso : LeftLift f' g'`. -/
+def ofIso (t : LeftLift f g) : LeftLift f' g' :=
+  (mapIso ef eg).functor.obj t
+
+@[simp]
+theorem ofIso_lift (t : LeftLift f g) :
+    (t.ofIso ef eg).lift = t.lift :=
+  rfl
+
+@[simp]
+theorem ofIso_unit (t : LeftLift f g) :
+    (t.ofIso ef eg).unit = eg.inv ≫ t.unit ≫ t.lift ◁ ef.hom :=
+  rfl
+
+/-- Whiskering commutes with `LeftLift.ofIso`. -/
+def whiskerOfIso (t : LeftLift f g) {x : B} (h : x ⟶ c) :
+    (t.whisker h).ofIso ef (whiskerLeftIso h eg) ≅ (t.ofIso ef eg).whisker h :=
+  StructuredArrow.isoMk (Iso.refl _) <| by simp [postcomp]
+
+end OfIso
+
 end LeftLift
 
 /-- Triangle diagrams for (right) extensions.
@@ -310,15 +372,16 @@ abbrev counit (t : RightExtension f g) : f ≫ t.extension ⟶ g := t.hom
 abbrev mk (h : b ⟶ c) (counit : f ≫ h ⟶ g) : RightExtension f g :=
   CostructuredArrow.mk counit
 
+variable {s t : RightExtension f g}
+
 /-- To construct a morphism between right extensions, we need a 2-morphism between the extensions,
 and to check that it is compatible with the counits. -/
-abbrev homMk {s t : RightExtension f g} (η : s.extension ⟶ t.extension)
+abbrev homMk (η : s.extension ⟶ t.extension)
     (w : f ◁ η ≫ t.counit = s.counit := by cat_disch) : s ⟶ t :=
   CostructuredArrow.homMk η w
 
 @[reassoc (attr := simp)]
-theorem w {s t : RightExtension f g} (η : s ⟶ t) :
-    f ◁ η.left ≫ t.counit = s.counit :=
+theorem w (η : s ⟶ t) : f ◁ η.left ≫ t.counit = s.counit :=
   CostructuredArrow.w η
 
 /-- The right extension along the identity. -/
@@ -326,6 +389,112 @@ def alongId (g : a ⟶ c) : RightExtension (𝟙 a) g := .mk _ (λ_ g).hom
 
 instance : Inhabited (RightExtension (𝟙 a) g) := ⟨alongId g⟩
 
+/-- Construct a right extension of `g : a ⟶ c` from a right extension of `g ≫ 𝟙 c`. -/
+@[simps!]
+def ofCompId (t : RightExtension f (g ≫ 𝟙 c)) : RightExtension f g :=
+  mk (extension t) (counit t ≫ (ρ_ g).hom)
+
+/-- Whisker a 1-morphism to an extension.
+```
+  b
+  △ \
+  |   \ extension  | counit
+f |     \          ▽
+  |       ◿
+  a - - - ▷ c - - - ▷ x
+      g         h
+```
+-/
+def whisker (t : RightExtension f g) {x : B} (h : c ⟶ x) : RightExtension f (g ≫ h) :=
+  .mk _ <| (α_ f t.extension h).inv ≫ t.counit ▷ h
+
+@[simp]
+theorem whisker_extension (t : RightExtension f g) {x : B} (h : c ⟶ x) :
+    (t.whisker h).extension = t.extension ≫ h :=
+  rfl
+
+@[simp]
+theorem whisker_counit (t : RightExtension f g) {x : B} (h : c ⟶ x) :
+    (t.whisker h).counit = (α_ f t.extension h).inv ≫ t.counit ▷ h :=
+  rfl
+
+/-- Whiskering a 1-morphism is a functor. -/
+@[simps]
+def whiskering {x : B} (h : c ⟶ x) : RightExtension f g ⥤ RightExtension f (g ≫ h) where
+  obj t := t.whisker h
+  map η := RightExtension.homMk (η.left ▷ h) <| by
+    simp [-RightExtension.w, ← RightExtension.w η]
+
+set_option backward.isDefEq.respectTransparency false in
+/-- Define a morphism between right extensions by cancelling the whiskered identities. -/
+@[simps! left]
+def whiskerIdCancel
+    (t : RightExtension f (g ≫ 𝟙 c)) {s : RightExtension f g} (τ : s.whisker (𝟙 c) ⟶ t) :
+    s ⟶ t.ofCompId :=
+  RightExtension.homMk ((ρ_ _).inv ≫ τ.left)
+
+set_option backward.isDefEq.respectTransparency false in
+/-- Construct a morphism between whiskered extensions. -/
+@[simps! left]
+def whiskerHom (i : s ⟶ t) {x : B} (h : c ⟶ x) :
+    s.whisker h ⟶ t.whisker h :=
+  CostructuredArrow.homMk (i.left ▷ h) <| by
+    rw [← cancel_epi (α_ f s.extension h).hom]
+    calc
+      _ = (f ◁ i.left ≫ t.counit) ▷ h := by simp [-RightExtension.w]
+      _ = s.counit ▷ h := congrArg (· ▷ h) (RightExtension.w i)
+      _ = _ := by simp
+
+/-- Construct an isomorphism between whiskered extensions. -/
+def whiskerIso (i : s ≅ t) {x : B} (h : c ⟶ x) :
+    s.whisker h ≅ t.whisker h :=
+  Iso.mk (whiskerHom i.hom h) (whiskerHom i.inv h)
+    (CostructuredArrow.hom_ext _ _ <|
+      calc
+        _ = (i.hom ≫ i.inv).left ▷ h := by simp [-Iso.hom_inv_id]
+        _ = 𝟙 _ := by simp [Iso.hom_inv_id])
+    (CostructuredArrow.hom_ext _ _ <|
+      calc
+        _ = (i.inv ≫ i.hom).left ▷ h := by simp [-Iso.inv_hom_id]
+        _ = 𝟙 _ := by simp [Iso.inv_hom_id])
+
+set_option backward.defeqAttrib.useBackward true in
+/-- The isomorphism between right extensions induced by a right unitor. -/
+@[simps! hom_left inv_left]
+def whiskerOfCompIdIsoSelf (t : RightExtension f g) : (t.whisker (𝟙 c)).ofCompId ≅ t :=
+  CostructuredArrow.isoMk (ρ_ (t.extension))
+
+section OfIso
+
+variable {f f' : a ⟶ b} (ef : f ≅ f') {g g' : a ⟶ c} (eg : g ≅ g')
+
+/-- Given isomorphisms `ef : f ≅ f'` and `eg : g ≅ g'`, the induced equivalence between their
+categories of right extensions. -/
+def mapIso : RightExtension f g ≌ RightExtension f' g' :=
+  (CostructuredArrow.mapNatIso ((precomposing a b c).mapIso ef)).trans (CostructuredArrow.mapIso eg)
+
+/-- Given isomorphisms `ef : f ≅ f'` and `eg : g ≅ g'`, and a right extension
+`t : RightExtension f g`, the induced right extension `t.ofIso : RightExtension f' g'`. -/
+def ofIso (t : RightExtension f g) : RightExtension f' g' :=
+  (mapIso ef eg).functor.obj t
+
+@[simp]
+theorem ofIso_extension (t : RightExtension f g) :
+    (t.ofIso ef eg).extension = t.extension :=
+  rfl
+
+@[simp]
+theorem ofIso_counit (t : RightExtension f g) :
+    (t.ofIso ef eg).counit = ef.inv ▷ t.extension ≫ t.counit ≫ eg.hom := by
+  rw [← Category.assoc]; rfl
+
+/-- Whiskering commutes with `RightExtension.ofIso`. -/
+def whiskerOfIso (t : RightExtension f g) {x : B} (h : c ⟶ x) :
+    (t.whisker h).ofIso ef (whiskerRightIso eg h) ≅ (t.ofIso ef eg).whisker h :=
+  CostructuredArrow.isoMk (Iso.refl _) <| by simp [precomp]
+
+end OfIso
+
 end RightExtension
 
 /-- Triangle diagrams for (right) lifts.
@@ -449,6 +618,38 @@ set_option backward.defeqAttrib.useBackward true in
 def whiskerOfIdCompIsoSelf (t : RightLift f g) : (t.whisker (𝟙 c)).ofIdComp ≅ t :=
   CostructuredArrow.isoMk (λ_ (lift t))
 
+section OfIso
+
+variable {f f' : b ⟶ a} (ef : f ≅ f') {g g' : c ⟶ a} (eg : g ≅ g')
+
+/-- Given isomorphisms `ef : f ≅ f'` and `eg : g ≅ g'`, the induced equivalence between their
+categories of right lifts. -/
+def mapIso : RightLift f g ≌ RightLift f' g' :=
+  (CostructuredArrow.mapNatIso ((postcomposing c b a).mapIso ef)).trans
+    (CostructuredArrow.mapIso eg)
+
+/-- Given isomorphisms `ef : f ≅ f'` and `eg : g ≅ g'`, and a right lift `t : RightLift f g`, the
+induced right lift `t.ofIso : RightLift f' g'`. -/
+def ofIso (t : RightLift f g) : RightLift f' g' :=
+  (mapIso ef eg).functor.obj t
+
+@[simp]
+theorem ofIso_lift (t : RightLift f g) :
+    (t.ofIso ef eg).lift = t.lift :=
+  rfl
+
+@[simp]
+theorem ofIso_counit (t : RightLift f g) :
+    (t.ofIso ef eg).counit = t.lift ◁ ef.inv ≫ t.counit ≫ eg.hom := by
+  rw [← Category.assoc]; rfl
+
+/-- Whiskering commutes with `RightLift.ofIso`. -/
+def whiskerOfIso (t : RightLift f g) {x : B} (h : x ⟶ c) :
+    (t.whisker h).ofIso ef (whiskerLeftIso h eg) ≅ (t.ofIso ef eg).whisker h :=
+  CostructuredArrow.isoMk (Iso.refl _) <| by simp [postcomp]
+
+end OfIso
+
 end RightLift
 
 end Bicategory
diff --git a/Mathlib/CategoryTheory/Bicategory/Kan/IsKan.lean b/Mathlib/CategoryTheory/Bicategory/Kan/IsKan.lean
index 9e21f2f7917678..f679ddee572983 100644
--- a/Mathlib/CategoryTheory/Bicategory/Kan/IsKan.lean
+++ b/Mathlib/CategoryTheory/Bicategory/Kan/IsKan.lean
@@ -5,7 +5,9 @@ Authors: Yuma Mizuno
 -/
 module
 
+public import Mathlib.CategoryTheory.Adjunction.Limits
 public import Mathlib.CategoryTheory.Bicategory.Extension
+public import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
 
 /-!
 # Kan extensions and Kan lifts in bicategories
@@ -117,6 +119,11 @@ def whiskerOfCommute (s t : LeftExtension f g) (i : s ≅ t) {x : B} (h : c ⟶
     IsKan (t.whisker h) :=
   P.ofIsoKan <| whiskerIso i h
 
+/-- `LeftExtension.ofIso` preserves Kan extensions. -/
+noncomputable def ofIso {f' : a ⟶ b} {g' : a ⟶ c} (H : IsKan t) (ef : f ≅ f') (eg : g ≅ g') :
+    IsKan (t.ofIso ef eg) :=
+  Limits.IsInitial.isInitialObj (LeftExtension.mapIso ef eg).functor t H
+
 end IsKan
 
 namespace IsAbsKan
@@ -137,6 +144,11 @@ of extensions. -/
 def ofIsoAbsKan (P : IsAbsKan s) (i : s ≅ t) : IsAbsKan t :=
   fun h ↦ (P h).ofIsoKan (whiskerIso i h)
 
+/-- `LeftExtension.ofIso` preserves absolute left Kan extensions. -/
+noncomputable def ofIso {f' : a ⟶ b} {g' : a ⟶ c} (H : IsAbsKan t) (ef : f ≅ f') (eg : g ≅ g') :
+    IsAbsKan (t.ofIso ef eg) :=
+  fun h ↦ ((H h).ofIso ef (whiskerRightIso eg h)).ofIsoKan (whiskerOfIso ef eg t h)
+
 end IsAbsKan
 
 end LeftExtension
@@ -209,6 +221,11 @@ def whiskerOfCommute (s t : LeftLift f g) (i : s ≅ t) {x : B} (h : x ⟶ c)
     IsKan (t.whisker h) :=
   P.ofIsoKan <| whiskerIso i h
 
+/-- `LeftLift.ofIso` preserves Kan lifts. -/
+noncomputable def ofIso {f' : b ⟶ a} {g' : c ⟶ a} (H : IsKan t) (ef : f ≅ f') (eg : g ≅ g') :
+    IsKan (t.ofIso ef eg) :=
+  Limits.IsInitial.isInitialObj (LeftLift.mapIso ef eg).functor t H
+
 end IsKan
 
 namespace IsAbsKan
@@ -228,6 +245,11 @@ def isKan (H : IsAbsKan t) : IsKan t :=
 def ofIsoAbsKan (P : IsAbsKan s) (i : s ≅ t) : IsAbsKan t :=
   fun h ↦ (P h).ofIsoKan (whiskerIso i h)
 
+/-- `LeftLift.ofIso` preserves absolute left Kan lifts. -/
+noncomputable def ofIso {f' : b ⟶ a} {g' : c ⟶ a} (H : IsAbsKan t) (ef : f ≅ f') (eg : g ≅ g') :
+    IsAbsKan (t.ofIso ef eg) :=
+  fun h ↦ ((H h).ofIso ef (whiskerLeftIso h eg)).ofIsoKan (whiskerOfIso ef eg t h)
+
 end IsAbsKan
 
 end LeftLift
@@ -239,6 +261,100 @@ variable {f : a ⟶ b} {g : a ⟶ c}
 /-- A right Kan extension of `g` along `f` is a terminal object in `RightExtension f g`. -/
 abbrev IsKan (t : RightExtension f g) := t.IsUniversal
 
+/-- An absolute right Kan extension is a Kan extension that commutes with any 1-morphism. -/
+abbrev IsAbsKan (t : RightExtension f g) :=
+  ∀ {x : B} (h : c ⟶ x), IsKan (t.whisker h)
+
+namespace IsKan
+
+variable {s t : RightExtension f g}
+
+/-- To show that a right extension `t` is a Kan extension, we need to show that for every right
+extension `s` there is a unique morphism `s ⟶ t`. -/
+abbrev mk (desc : ∀ s, s ⟶ t) (w : ∀ s τ, τ = desc s) :
+    IsKan t :=
+  .ofUniqueHom desc w
+
+/-- The family of 2-morphisms into a right Kan extension. -/
+abbrev desc (H : IsKan t) (s : RightExtension f g) : s.extension ⟶ t.extension :=
+  CostructuredArrow.IsUniversal.lift H s
+
+@[reassoc (attr := simp)]
+theorem fac (H : IsKan t) (s : RightExtension f g) :
+    f ◁ H.desc s ≫ t.counit = s.counit :=
+  CostructuredArrow.IsUniversal.fac H s
+
+/-- Two 2-morphisms into a right Kan extension are equal if their compositions with
+each triangle 2-morphism are equal. -/
+theorem hom_ext (H : IsKan t) {k : b ⟶ c} {τ τ' : k ⟶ t.extension}
+    (w : f ◁ τ ≫ t.counit = f ◁ τ' ≫ t.counit) : τ = τ' :=
+  CostructuredArrow.IsUniversal.hom_ext H w
+
+/-- Kan extensions on `g` along `f` are unique up to isomorphism. -/
+def uniqueUpToIso (P : IsKan s) (Q : IsKan t) : s ≅ t :=
+  Limits.IsTerminal.uniqueUpToIso P Q
+
+@[simp]
+theorem uniqueUpToIso_hom_left (P : IsKan s) (Q : IsKan t) :
+    (uniqueUpToIso P Q).hom.left = Q.desc s := rfl
+
+@[simp]
+theorem uniqueUpToIso_inv_left (P : IsKan s) (Q : IsKan t) :
+    (uniqueUpToIso P Q).inv.left = P.desc t := rfl
+
+/-- Transport evidence that a right extension is a Kan extension across an isomorphism
+of extensions. -/
+def ofIsoKan (P : IsKan s) (i : s ≅ t) : IsKan t :=
+  Limits.IsTerminal.ofIso P i
+
+set_option backward.isDefEq.respectTransparency false in
+/-- If `t : RightExtension f (g ≫ 𝟙 c)` is a Kan extension, then `t.ofCompId : RightExtension f g`
+is also a Kan extension. -/
+def ofCompId (t : RightExtension f (g ≫ 𝟙 c)) (P : IsKan t) : IsKan t.ofCompId :=
+  .mk (fun s ↦ t.whiskerIdCancel <| P.from (s.whisker (𝟙 c))) <| by
+    intro s τ
+    ext
+    apply P.hom_ext
+    simp [← RightExtension.w τ]
+
+/-- If `s ≅ t` and `IsKan (s.whisker h)`, then `IsKan (t.whisker h)`. -/
+def whiskerOfCommute (s t : RightExtension f g) (i : s ≅ t) {x : B} (h : c ⟶ x)
+    (P : IsKan (s.whisker h)) :
+    IsKan (t.whisker h) :=
+  P.ofIsoKan <| whiskerIso i h
+
+/-- `RightExtension.ofIso` preserves Kan extensions. -/
+noncomputable def ofIso {f' : a ⟶ b} {g' : a ⟶ c} (H : IsKan t) (ef : f ≅ f') (eg : g ≅ g') :
+    IsKan (t.ofIso ef eg) :=
+  Limits.IsTerminal.isTerminalObj (RightExtension.mapIso ef eg).functor t H
+
+end IsKan
+
+namespace IsAbsKan
+
+variable {s t : RightExtension f g}
+
+/-- The family of 2-morphisms into an absolute right Kan extension. -/
+abbrev desc (H : IsAbsKan t) {x : B} {h : c ⟶ x} (s : RightExtension f (g ≫ h)) :
+    s.extension ⟶ t.extension ≫ h :=
+  (H h).desc s
+
+/-- An absolute right Kan extension is a right Kan extension. -/
+def isKan (H : IsAbsKan t) : IsKan t :=
+  ((H (𝟙 c)).ofCompId _).ofIsoKan <| whiskerOfCompIdIsoSelf t
+
+/-- Transport evidence that a right extension is a Kan extension across an isomorphism
+of extensions. -/
+def ofIsoAbsKan (P : IsAbsKan s) (i : s ≅ t) : IsAbsKan t :=
+  fun h ↦ (P h).ofIsoKan (whiskerIso i h)
+
+/-- `RightExtension.ofIso` preserves absolute right Kan extensions. -/
+noncomputable def ofIso {f' : a ⟶ b} {g' : a ⟶ c} (H : IsAbsKan t) (ef : f ≅ f') (eg : g ≅ g') :
+    IsAbsKan (t.ofIso ef eg) :=
+  fun h ↦ ((H h).ofIso ef (whiskerRightIso eg h)).ofIsoKan (whiskerOfIso ef eg t h)
+
+end IsAbsKan
+
 end RightExtension
 
 namespace RightLift
@@ -309,6 +425,11 @@ def whiskerOfCommute (s t : RightLift f g) (i : s ≅ t) {x : B} (h : x ⟶ c)
     IsKan (t.whisker h) :=
   P.ofIsoKan <| whiskerIso i h
 
+/-- `RightLift.ofIso` preserves Kan lifts. -/
+noncomputable def ofIso {f' : b ⟶ a} {g' : c ⟶ a} (H : IsKan t) (ef : f ≅ f') (eg : g ≅ g') :
+    IsKan (t.ofIso ef eg) :=
+  Limits.IsTerminal.isTerminalObj (RightLift.mapIso ef eg).functor t H
+
 end IsKan
 
 namespace IsAbsKan
@@ -328,6 +449,11 @@ def isKan (H : IsAbsKan t) : IsKan t :=
 def ofIsoAbsKan (P : IsAbsKan s) (i : s ≅ t) : IsAbsKan t :=
   fun h ↦ (P h).ofIsoKan (whiskerIso i h)
 
+/-- `RightLift.ofIso` preserves absolute right Kan lifts. -/
+noncomputable def ofIso {f' : b ⟶ a} {g' : c ⟶ a} (H : IsAbsKan t) (ef : f ≅ f') (eg : g ≅ g') :
+    IsAbsKan (t.ofIso ef eg) :=
+  fun h ↦ ((H h).ofIso ef (whiskerLeftIso h eg)).ofIsoKan (whiskerOfIso ef eg t h)
+
 end IsAbsKan
 
 end RightLift