S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category S
inst✝⁴ : Category L
inst✝³ : Category D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasColimitsOfShape (CostructuredArrow ι X) D
this : ∀ (X : S ⥤ D), IsIso ((adjunction D ι).unit.app X)
⊢ IsIso (adjunction D ι).unit

case this
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category S
inst✝⁴ : Category L
inst✝³ : Category D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasColimitsOfShape (CostructuredArrow ι X) D
⊢ ∀ (X : S ⥤ D), IsIso ((adjunction D ι).unit.app X)
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category S
inst✝⁴ : Category L
inst✝³ : Category D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasColimitsOfShape (CostructuredArrow ι X) D
⊢ IsIso (adjunction D ι).unit
suffices : ∀ (X : S ⥤ D), IsIso (NatTrans.app (adjunction D ι).unit X)
case this
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category S
inst✝⁴ : Category L
inst✝³ : Category D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasColimitsOfShape (CostructuredArrow ι X) D
F : S ⥤ D
⊢ IsIso ((adjunction D ι).unit.app F)
case this
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category S
inst✝⁴ : Category L
inst✝³ : Category D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasColimitsOfShape (CostructuredArrow ι X) D
⊢ ∀ (X : S ⥤ D), IsIso ((adjunction D ι).unit.app X)
intro F
case this
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category S
inst✝⁴ : Category L
inst✝³ : Category D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasColimitsOfShape (CostructuredArrow ι X) D
F : S ⥤ D
this : ∀ (X : S), IsIso (((adjunction D ι).unit.app F).app X)
⊢ IsIso ((adjunction D ι).unit.app F)

case this
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category S
inst✝⁴ : Category L
inst✝³ : Category D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasColimitsOfShape (CostructuredArrow ι X) D
F : S ⥤ D
⊢ ∀ (X : S), IsIso (((adjunction D ι).unit.app F).app X)
case this
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category S
inst✝⁴ : Category L
inst✝³ : Category D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasColimitsOfShape (CostructuredArrow ι X) D
F : S ⥤ D
⊢ IsIso ((adjunction D ι).unit.app F)
suffices : ∀ (X : S), IsIso (NatTrans.app (NatTrans.app (adjunction D ι).unit F) X)
case this
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category S
inst✝⁴ : Category L
inst✝³ : Category D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasColimitsOfShape (CostructuredArrow ι X) D
F : S ⥤ D
X : S
⊢ IsIso (((adjunction D ι).unit.app F).app X)
case this
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category S
inst✝⁴ : Category L
inst✝³ : Category D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasColimitsOfShape (CostructuredArrow ι X) D
F : S ⥤ D
⊢ ∀ (X : S), IsIso (((adjunction D ι).unit.app F).app X)
intro X
case this
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category S
inst✝⁴ : Category L
inst✝³ : Category D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasColimitsOfShape (CostructuredArrow ι X) D
F : S ⥤ D
X : S
⊢ IsIso (colimit.ι (diagram ι F (ι.obj X)) (CostructuredArrow.mk (𝟙 (ι.obj X))) ≫ 𝟙 (colimit (diagram ι F (ι.obj X))))
case this
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category S
inst✝⁴ : Category L
inst✝³ : Category D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasColimitsOfShape (CostructuredArrow ι X) D
F : S ⥤ D
X : S
⊢ IsIso (((adjunction D ι).unit.app F).app X)
dsimp [adjunction, equiv]
case this
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category S
inst✝⁴ : Category L
inst✝³ : Category D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasColimitsOfShape (CostructuredArrow ι X) D
F : S ⥤ D
X : S
⊢ IsIso (colimit.ι (diagram ι F (ι.obj X)) (CostructuredArrow.mk (𝟙 (ι.obj X))))
case this
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category S
inst✝⁴ : Category L
inst✝³ : Category D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasColimitsOfShape (CostructuredArrow ι X) D
F : S ⥤ D
X : S
⊢ IsIso (colimit.ι (diagram ι F (ι.obj X)) (CostructuredArrow.mk (𝟙 (ι.obj X))) ≫ 𝟙 (colimit (diagram ι F (ι.obj X))))
simp only [Category.comp_id]
no goals
case this
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category S
inst✝⁴ : Category L
inst✝³ : Category D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasColimitsOfShape (CostructuredArrow ι X) D
F : S ⥤ D
X : S
⊢ IsIso (colimit.ι (diagram ι F (ι.obj X)) (CostructuredArrow.mk (𝟙 (ι.obj X))))
exact
  IsIso.of_iso
    ((colimit.isColimit _).coconePointUniqueUpToIso
        (colimitOfDiagramTerminal CostructuredArrow.mkIdTerminal _)).symm
no goals
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category S
inst✝⁴ : Category L
inst✝³ : Category D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasColimitsOfShape (CostructuredArrow ι X) D
this : ∀ (X : S ⥤ D), IsIso ((adjunction D ι).unit.app X)
⊢ IsIso (adjunction D ι).unit
apply NatIso.isIso_of_isIso_app
no goals
case this
S : Type u₁
L : Type u₂
D : Type u₃
inst✝⁵ : Category S
inst✝⁴ : Category L
inst✝³ : Category D
ι : S ⥤ L
inst✝² : Full ι
inst✝¹ : Faithful ι
inst✝ : ∀ (X : L), HasColimitsOfShape (CostructuredArrow ι X) D
F : S ⥤ D
this : ∀ (X : S), IsIso (((adjunction D ι).unit.app F).app X)
⊢ IsIso ((adjunction D ι).unit.app F)
apply NatIso.isIso_of_isIso_app