add right Kan extensions and so on

Mathlib/CategoryTheory/Bicategory/Extension.lean

@@ -25,8 +25,6 @@ is an alias for `Comma.right`.
 * https://ncatlab.org/nlab/show/lifts+and+extensions
 * https://ncatlab.org/nlab/show/Kan+extension
 
-## Todo
-API for left lifts, right extensions, and right lifts
 -/
 
 namespace CategoryTheory
@@ -90,6 +88,11 @@ abbrev lift (t : LeftLift f g) : c ⟶ b := t.right
 /-- The 2-morphism filling the triangle diagram. -/
 abbrev unit (t : LeftLift f g) : g ⟶ t.lift ≫ f := t.hom
 
+/-- The left lift along the identity. -/
+def alongId (g : c ⟶ a) : LeftLift (𝟙 a) g := StructuredArrow.mk (ρ_ g).inv
+
+instance : Inhabited (LeftLift (𝟙 a) g) := ⟨alongId g⟩
+
 end LeftLift
 
 /-- Triangle diagrams for (right) extensions.
@@ -115,6 +118,11 @@ abbrev extension (t : RightExtension f g) : b ⟶ c := t.left
 /-- The 2-morphism filling the triangle diagram. -/
 abbrev counit (t : RightExtension f g) : f ≫ t.extension ⟶ g := t.hom
 
+/-- The right extension along the identity. -/
+def alongId (g : a ⟶ c) : RightExtension (𝟙 a) g := CostructuredArrow.mk (λ_ g).hom
+
+instance : Inhabited (RightExtension (𝟙 a) g) := ⟨alongId g⟩
+
 end RightExtension
 
 /-- Triangle diagrams for (right) lifts.
@@ -140,6 +148,11 @@ abbrev lift (t : RightLift f g) : c ⟶ b := t.left
 /-- The 2-morphism filling the triangle diagram. -/
 abbrev counit (t : RightLift f g) : t.lift ≫ f ⟶ g := t.hom
 
+/-- The right lift along the identity. -/
+def alongId (g : c ⟶ a) : RightLift (𝟙 a) g := CostructuredArrow.mk (ρ_ g).hom
+
+instance : Inhabited (RightLift (𝟙 a) g) := ⟨alongId g⟩
+
 end RightLift
 
 end Bicategory

Mathlib/CategoryTheory/Bicategory/IsKan.lean

@@ -20,6 +20,8 @@ in the namespace `StructuredArrow.IsUniversal`:
 * `h.hom_ext`: two 2-morphisms out of the left Kan extension are equal if their compositions with
   each unit are equal.
 
+We also define left Kan lifts, right Kan extensions, and right Kan lifts.
+
 ## Implementation Notes
 We use the Is-Has design pattern, which is used for the implementation of limits and colimits in
 the category theory library. This means that `IsKan t` is a structure containing the data of
@@ -30,8 +32,6 @@ exists.
 ## References
 https://ncatlab.org/nlab/show/Kan+extension
 
-## Todo
-left Kan lifts, right Kan extensions, and right Kan lifts
 -/
 
 namespace CategoryTheory
@@ -51,6 +51,33 @@ abbrev IsKan (t : LeftExtension f g) := t.IsUniversal
 
 end LeftExtension
 
+namespace LeftLift
+
+variable {f : b ⟶ a} {g : c ⟶ a}
+
+/-- A left Kan lift of `g` along `f` is an initial object in `LeftLift f g`. -/
+abbrev IsKan (t : LeftLift f g) := t.IsUniversal
+
+end LeftLift
+
+namespace RightExtension
+
+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
+
+end RightExtension
+
+namespace RightLift
+
+variable {f : b ⟶ a} {g : c ⟶ a}
+
+/-- A right Kan lift of `g` along `f` is a terminal object in `RightLift f g`. -/
+abbrev IsKan (t : RightLift f g) := t.IsUniversal
+
+end RightLift
+
 end Bicategory
 
 end CategoryTheory