Displayed Category

Given a type family F : C → Type* on a category C we define the type class Display F of displayed categories over F. A displayed category structure associates to each morphism f in C and terms X : F c and Y : F d a type HomOver f X Y whose terms are to be thought of as morphisms lying over f starting from X and ending at Y. The data of a displayed category structure also provides the dependent operations of identity and composition for HomOver. Finally, the modified laws of associativity and unitality hold, up to casting, dependently over the associativity and unitality equalities in C.

Our main construction is the displayed category of a functor. Given a functor P : E ⥤ C, the associated displayed category on the fiber family fun c => P⁻¹ c is provided by the instance instDisplayOfFunctor. Here HomOver f X Y is given by the type BasedLift f src tgt carrying data witnessing morphisms in E starting from src and ending at tgt and are mapped to f under P.

We also provide various useful constructors for based-lifts:

• BasedLift.tauto regards a morphism g of the domain category E as a tautological based-lift of its image P.map g.
• BasedLift.id and BasedLift.comp provide the identity and composition of based-lifts, respectively.
• We can cast a based-lift along an equality of the base morphisms using the equivalence BasedLift.cast.

We provide the following notations:

• X ⟶[f] Y for DisplayStruct.HomOver f x y
• f ≫ₗ g for DisplayStruct.comp_over f g

We show that for a functor P, the type BasedLift P induces a display category structure on the fiber family fun c => P⁻¹ c.

def CategoryTheory.Fiber {C : Type u_1} (F : C → Type u_2) (I : C) : Type u_2

Equations

• CategoryTheory.Fiber F I = F I

def CategoryTheory.fiberCast {C : Type u_1} (F : C → Type u_2) {I : C} {I' : C} (w : I = I') (X : F I) : F I'

Cast an element of a fiber along an equality of the base objects.

Equations

• CategoryTheory.fiberCast F w X = w ▸ X

def CategoryTheory.eqToHomMap {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {I : C} {I' : C} {J : C} {J' : C} (w : I = I') (w' : J = J') (f : I ⟶ J) : I' ⟶ J'

Transporting a morphism f : I ⟶ J along equalities w : I = I' and w' : J = J'. Note: It might be a good idea to add this to eqToHom file.

Equations

• CategoryTheory.eqToHomMap w w' f = w' ▸ w ▸ f

@[simp]

def CategoryTheory.eqToHomMapId {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {I : C} {I' : C} (w : I = I') : w ▸ CategoryTheory.CategoryStruct.id I = CategoryTheory.CategoryStruct.id I'

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.eqToHomMap_naturality {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {I : C} {I' : C} {J : C} {J' : C} {w : I = I'} {w' : J = J'} (f : I ⟶ J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom w) (CategoryTheory.eqToHomMap w w' f) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom w')

@[simp]

theorem CategoryTheory.fiber_cast_trans {C : Type u_1} (F : C → Type u_2) {I : C} {I' : C} {I'' : C} (X : F I) {w : I = I'} {w' : I' = I''} {w'' : I = I''} : w' ▸ w ▸ X = w'' ▸ X

theorem CategoryTheory.fiber_cast_cast {C : Type u_1} (F : C → Type u_2) {I : C} {I' : C} (X : F I) {w : I = I'} {w' : I' = I} : w' ▸ w ▸ X = X

class CategoryTheory.DisplayStruct {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (F : C → Type u_2) : Type (max (max (max u_1 u_2) (u_3 + 1)) u_4)

• HomOver : {I J : C} → (I ⟶ J) → F I → F J → Type u_3

  The type of morphisms indexed over morphisms of C.

• id_over : {I : C} → (X : F I) → X ⟶[CategoryTheory.CategoryStruct.id I] X

  The identity morphism overlying the identity morphism of C.

• comp_over : {I J K : C} → {f₁ : I ⟶ J} → {f₂ : J ⟶ K} → {X : F I} → {Y : F J} → {Z : F K} → (X ⟶[f₁] Y) → (Y ⟶[f₂] Z) → X ⟶[CategoryTheory.CategoryStruct.comp f₁ f₂] Z

  Composition of morphisms overlying composition of morphisms of C.

def CategoryTheory.«term_⟶[_]_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.«term𝟙ₗ» : Lean.ParserDescr

Equations

• CategoryTheory.«term𝟙ₗ» = Lean.ParserDescr.node `CategoryTheory.term𝟙ₗ 1024 (Lean.ParserDescr.symbol " 𝟙ₗ ")

def CategoryTheory.«term_≫ₗ_» : Lean.TrailingParserDescr

Equations

• CategoryTheory.«term_≫ₗ_» = Lean.ParserDescr.trailingNode `CategoryTheory.term_≫ₗ_ 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≫ₗ ") (Lean.ParserDescr.cat `term 80))

class CategoryTheory.Display {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (F : C → Type u_2) extends CategoryTheory.DisplayStruct : Type (max (max (max u_1 u_2) u_3) (u_4 + 1))

• HomOver : {I J : C} → (I ⟶ J) → F I → F J → Type u_4
• id_over : {I : C} → (X : F I) → X ⟶[CategoryTheory.CategoryStruct.id I] X
• comp_over : {I J K : C} → {f₁ : I ⟶ J} → {f₂ : J ⟶ K} → {X : F I} → {Y : F J} → {Z : F K} → (X ⟶[f₁] Y) → (Y ⟶[f₂] Z) → X ⟶[CategoryTheory.CategoryStruct.comp f₁ f₂] Z
• id_comp_cast : ∀ {I J : C} {f : I ⟶ J} {X : F I} {Y : F J} (g : X ⟶[f] Y), CategoryTheory.DisplayStruct.comp_over ( 𝟙ₗ X) g = ⋯ ▸ g
• comp_id_cast : ∀ {I J : C} {f : I ⟶ J} {X : F I} {Y : F J} (g : X ⟶[f] Y), CategoryTheory.DisplayStruct.comp_over g ( 𝟙ₗ Y) = ⋯ ▸ g
• assoc_cast : ∀ {I J K L : C} {f₁ : I ⟶ J} {f₂ : J ⟶ K} {f₃ : K ⟶ L} {X : F I} {Y : F J} {Z : F K} {W : F L} (g₁ : X ⟶[f₁] Y) (g₂ : Y ⟶[f₂] Z) (g₃ : Z ⟶[f₃] W), CategoryTheory.DisplayStruct.comp_over (CategoryTheory.DisplayStruct.comp_over g₁ g₂) g₃ = ⋯ ▸ CategoryTheory.DisplayStruct.comp_over g₁ (CategoryTheory.DisplayStruct.comp_over g₂ g₃)

@[simp]

theorem CategoryTheory.Display.id_comp_cast {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [self : CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} {X : F I} {Y : F J} (g : X ⟶[f] Y) : CategoryTheory.DisplayStruct.comp_over ( 𝟙ₗ X) g = ⋯ ▸ g

@[simp]

theorem CategoryTheory.Display.comp_id_cast {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [self : CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} {X : F I} {Y : F J} (g : X ⟶[f] Y) : CategoryTheory.DisplayStruct.comp_over g ( 𝟙ₗ Y) = ⋯ ▸ g

@[simp]

theorem CategoryTheory.Display.assoc_cast {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [self : CategoryTheory.Display F] {I : C} {J : C} {K : C} {L : C} {f₁ : I ⟶ J} {f₂ : J ⟶ K} {f₃ : K ⟶ L} {X : F I} {Y : F J} {Z : F K} {W : F L} (g₁ : X ⟶[f₁] Y) (g₂ : Y ⟶[f₂] Z) (g₃ : Z ⟶[f₃] W) : CategoryTheory.DisplayStruct.comp_over (CategoryTheory.DisplayStruct.comp_over g₁ g₂) g₃ = ⋯ ▸ CategoryTheory.DisplayStruct.comp_over g₁ (CategoryTheory.DisplayStruct.comp_over g₂ g₃)

def CategoryTheory.HomOver.cast {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} {f' : I ⟶ J} {X : F I} {Y : F J} (w : f = f') (g : X ⟶[f] Y) : X ⟶[f'] Y

Equations

• CategoryTheory.HomOver.cast w g = w ▸ g

@[simp]

theorem CategoryTheory.HomOver.cast_trans {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} {f' : I ⟶ J} {f'' : I ⟶ J} {X : F I} {Y : F J} {w : f = f'} {w' : f' = f''} (g : X ⟶[f] Y) : w' ▸ w ▸ g = ⋯ ▸ g

theorem CategoryTheory.HomOver.cast_unique {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} {f' : I ⟶ J} {X : F I} {Y : F J} {w : f = f'} {w' : f = f'} (g : X ⟶[f] Y) : w ▸ g = w' ▸ g

theorem CategoryTheory.HomOver.cast_cast {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} {f' : I ⟶ J} {X : F I} {Y : F J} (w : f = f') (w' : f' = f) (g : X ⟶[f'] Y) : ⋯ ▸ ⋯ ▸ g = g

theorem CategoryTheory.HomOver.comp_id_eq_cast_id_comp {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} {X : F I} {Y : F J} (g : X ⟶[f] Y) : CategoryTheory.DisplayStruct.comp_over g ( 𝟙ₗ Y) = CategoryTheory.HomOver.cast ⋯ (CategoryTheory.DisplayStruct.comp_over ( 𝟙ₗ X) g)

def CategoryTheory.HomOver.eqToHom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {I : C} {I' : C} (w : I = I') (X : F I) : X ⟶[CategoryTheory.eqToHom w] w ▸ X

EqToHom w X is a hom-over eqToHom w from X to w ▸ X.

Equations

• CategoryTheory.HomOver.eqToHom w X = w ▸ 𝟙ₗ X

def CategoryTheory.HomOver.eqToHomMap {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {I : C} {J : C} {I' : C} {J' : C} (w : I = I') (w' : J = J') {f : I ⟶ J} {X : F I} {Y : F J} (g : X ⟶[f] Y) : (w ▸ X) ⟶[CategoryTheory.eqToHomMap w w' f] w' ▸ Y

Equations

• CategoryTheory.HomOver.eqToHomMap w w' g = w ▸ w' ▸ g

def CategoryTheory.HomOver.eqToHomMapId {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {I : C} {I' : C} (w : I = I') {X : F I} {Y : F I} (g : X ⟶[CategoryTheory.CategoryStruct.id I] Y) : (w ▸ X) ⟶[CategoryTheory.CategoryStruct.id I'] w ▸ Y

Equations

• CategoryTheory.HomOver.eqToHomMapId w g = w ▸ g

theorem CategoryTheory.HomOver.eqToHom_naturality {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {I : C} {J : C} {I' : C} {J' : C} {X : F I} {Y : F J} (w : I = I') (w' : J = J') (f : I ⟶ J) (g : X ⟶[f] Y) : CategoryTheory.DisplayStruct.comp_over g (CategoryTheory.HomOver.eqToHom w' Y) = CategoryTheory.HomOver.cast ⋯ (CategoryTheory.DisplayStruct.comp_over (CategoryTheory.HomOver.eqToHom w X) (CategoryTheory.HomOver.eqToHomMap w w' g))

@[simp]

theorem CategoryTheory.HomOver.castEquiv_symm_apply {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} {f' : I ⟶ J} {X : F I} {Y : F J} (w : f = f') (g : X ⟶[f'] Y) : (CategoryTheory.HomOver.castEquiv w).symm g = ⋯ ▸ g

@[simp]

theorem CategoryTheory.HomOver.castEquiv_apply {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} {f' : I ⟶ J} {X : F I} {Y : F J} (w : f = f') (g : X ⟶[f] Y) : (CategoryTheory.HomOver.castEquiv w) g = w ▸ g

def CategoryTheory.HomOver.castEquiv {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} {f' : I ⟶ J} {X : F I} {Y : F J} (w : f = f') : (X ⟶[f] Y) ≃ X ⟶[f'] Y

Equations

• CategoryTheory.HomOver.castEquiv w = { toFun := fun (g : X ⟶[f] Y) => w ▸ g, invFun := fun (g : X ⟶[f'] Y) => ⋯ ▸ g, left_inv := ⋯, right_inv := ⋯ }

def CategoryTheory.Display.Total {C : Type u_1} (F : C → Type u_2) : Type (max u_1 u_2)

The total space of a displayed category consists of pairs (I, X) where I is an object of C and X is an object of the fiber over I.

Equations

• ∫ F = ((I : C) × F I)

def CategoryTheory.Display.«term∫_» : Lean.ParserDescr

Equations

• CategoryTheory.Display.«term∫_» = Lean.ParserDescr.node `CategoryTheory.Display.term∫_ 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∫ ") (Lean.ParserDescr.cat `term 75))

@[reducible, inline]

abbrev CategoryTheory.Display.TotalHom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] (X : ∫ F) (Y : ∫ F) : Type (max u_3 u_4)

Equations

• CategoryTheory.Display.TotalHom X Y = ((f : X.fst ⟶ Y.fst) × X.snd ⟶[f] Y.snd)

instance CategoryTheory.Display.instCategoryStructTotal {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] : CategoryTheory.CategoryStruct.{max u_4 u_3, max u_2 u_1} ( ∫ F)

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.Display.instPartialOrderHomTotal {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {X : ∫ F} {Y : ∫ F} : PartialOrder (X ⟶ Y)

Equations

• CategoryTheory.Display.instPartialOrderHomTotal = PartialOrder.mk ⋯

instance CategoryTheory.Display.instCategoryTotalHom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {X : ∫ F} {Y : ∫ F} : CategoryTheory.SmallCategory (X ⟶ Y)

Equations

• CategoryTheory.Display.instCategoryTotalHom = inferInstance

@[simp]

theorem CategoryTheory.Display.cast_exchange_comp {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {I : C} {J : C} {K : C} {f : I ⟶ J} {f' : I ⟶ J} {h : J ⟶ K} {h' : J ⟶ K} {X : F I} {Y : F J} {Z : F K} (g : X ⟶[f] Y) (k : Y ⟶[h] Z) (w : f = f') (w' : h = h') : w' ▸ CategoryTheory.DisplayStruct.comp_over g k = CategoryTheory.DisplayStruct.comp_over (⋯ ▸ ⋯ ▸ g) (w' ▸ k)

@[simp]

theorem CategoryTheory.Display.whisker_left_cast_comp {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {I : C} {J : C} {K : C} {f : I ⟶ J} {h : J ⟶ K} {h' : J ⟶ K} {X : F I} {Y : F J} {Z : F K} (g : X ⟶[f] Y) (k : Y ⟶[h] Z) (w : h = h') : ⋯ ▸ CategoryTheory.DisplayStruct.comp_over g k = CategoryTheory.DisplayStruct.comp_over g (w ▸ k)

@[simp]

theorem CategoryTheory.Display.whisker_right_cast_comp {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {I : C} {J : C} {K : C} {f : I ⟶ J} {f' : I ⟶ J} {h : J ⟶ K} {X : F I} {Y : F J} {Z : F K} (g : X ⟶[f] Y) (k : Y ⟶[h] Z) (w : f = f') : ⋯ ▸ CategoryTheory.DisplayStruct.comp_over g k = CategoryTheory.DisplayStruct.comp_over (w ▸ g) k

instance CategoryTheory.Display.instBicategoryTotal {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] : CategoryTheory.Bicategory ( ∫ F)

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.Display.instCategoryTotal {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] : CategoryTheory.Category.{max u_4 u_3, max u_2 u_1} ( ∫ F)

Equations

• CategoryTheory.Display.instCategoryTotal = CategoryTheory.Category.mk ⋯ ⋯ ⋯

instance CategoryTheory.Display.instCategoryFiber {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {I : C} : CategoryTheory.Category.{u_4, u_2} (F I)

The category structure on the fibers of a display category.

Equations

• CategoryTheory.Display.instCategoryFiber = CategoryTheory.Category.mk ⋯ ⋯ ⋯

def CategoryTheory.Display.Vert {C : Type u_1} (F : C → Type u_2) : Type (max u_1 u_2)

Equations

• CategoryTheory.Display.Vert F = ((I : C) × F I)

structure CategoryTheory.Display.VertHom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] (X : CategoryTheory.Display.Vert F) (Y : CategoryTheory.Display.Vert F) : Type u_4

• base_eq : X.fst = Y.fst
• over_id : X.snd ⟶[CategoryTheory.CategoryStruct.id X.fst] ⋯ ▸ Y.snd

theorem CategoryTheory.Display.VertHom.base_eq {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {X : CategoryTheory.Display.Vert F} {Y : CategoryTheory.Display.Vert F} (self : CategoryTheory.Display.VertHom X Y) : X.fst = Y.fst

instance CategoryTheory.Display.instCategoryVert {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] : CategoryTheory.Category.{u_4, max u_2 u_1} (CategoryTheory.Display.Vert F)

Equations

• CategoryTheory.Display.instCategoryVert = CategoryTheory.Category.mk ⋯ ⋯ ⋯

class CategoryTheory.Display.IsIso {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} [CategoryTheory.IsIso f] {X : F I} {Y : F J} (g : X ⟶[f] Y) : Prop

A hom-over of an isomorphism is invertible if

• out : ∃ (inv : Y ⟶[CategoryTheory.inv f] X), ⋯ ▸ CategoryTheory.DisplayStruct.comp_over g inv = 𝟙ₗ X ∧ ⋯ ▸ CategoryTheory.DisplayStruct.comp_over inv g = 𝟙ₗ Y

  The existence of an inverse hom-over.

theorem CategoryTheory.Display.IsIso.out {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} [CategoryTheory.IsIso f] {X : F I} {Y : F J} {g : X ⟶[f] Y} [self : CategoryTheory.Display.IsIso g] : ∃ (inv : Y ⟶[CategoryTheory.inv f] X), ⋯ ▸ CategoryTheory.DisplayStruct.comp_over g inv = 𝟙ₗ X ∧ ⋯ ▸ CategoryTheory.DisplayStruct.comp_over inv g = 𝟙ₗ Y

The existence of an inverse hom-over.

class CategoryTheory.IsoDisplay {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (F : C → Type u_2) extends CategoryTheory.Display : Type (max (max (max u_1 u_2) u_3) (u_4 + 1))

The IsoDisplay structure associated to a family F of types over a category C: A display category is iso-display if every hom-over an isomorphism is itself a display isomorphism.

• HomOver : {I J : C} → (I ⟶ J) → F I → F J → Type u_4
• id_over : {I : C} → (X : F I) → X ⟶[CategoryTheory.CategoryStruct.id I] X
• comp_over : {I J K : C} → {f₁ : I ⟶ J} → {f₂ : J ⟶ K} → {X : F I} → {Y : F J} → {Z : F K} → (X ⟶[f₁] Y) → (Y ⟶[f₂] Z) → X ⟶[CategoryTheory.CategoryStruct.comp f₁ f₂] Z
• id_comp_cast : ∀ {I J : C} {f : I ⟶ J} {X : F I} {Y : F J} (g : X ⟶[f] Y), CategoryTheory.DisplayStruct.comp_over ( 𝟙ₗ X) g = ⋯ ▸ g
• comp_id_cast : ∀ {I J : C} {f : I ⟶ J} {X : F I} {Y : F J} (g : X ⟶[f] Y), CategoryTheory.DisplayStruct.comp_over g ( 𝟙ₗ Y) = ⋯ ▸ g
• assoc_cast : ∀ {I J K L : C} {f₁ : I ⟶ J} {f₂ : J ⟶ K} {f₃ : K ⟶ L} {X : F I} {Y : F J} {Z : F K} {W : F L} (g₁ : X ⟶[f₁] Y) (g₂ : Y ⟶[f₂] Z) (g₃ : Z ⟶[f₃] W), CategoryTheory.DisplayStruct.comp_over (CategoryTheory.DisplayStruct.comp_over g₁ g₂) g₃ = ⋯ ▸ CategoryTheory.DisplayStruct.comp_over g₁ (CategoryTheory.DisplayStruct.comp_over g₂ g₃)
• iso_HomOver : ∀ {I J : C} {f : I ⟶ J} [inst : CategoryTheory.IsIso f] {X : F I} {Y : F J} (g : X ⟶[f] Y), CategoryTheory.Display.IsIso g

theorem CategoryTheory.IsoDisplay.iso_HomOver {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : C → Type u_2} [self : CategoryTheory.IsoDisplay F] {I : C} {J : C} {f : I ⟶ J} [CategoryTheory.IsIso f] {X : F I} {Y : F J} (g : X ⟶[f] Y) : CategoryTheory.Display.IsIso g