C : Type u
inst✝⁹ : Category C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category D
E : Type w₂
inst✝⁷ : Category E
F : D ⥤ E
G✝ : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
G : Type (max v u) ⥤ D
adj : G ⊣ forget D
Y : SheafOfTypes J
⊢ ((Equivalence.toAdjunction (Equivalence.symm (sheafEquivSheafOfTypes J))).unit.app Y).val ≫
      ((adjunction J adj).unit.app ((sheafEquivSheafOfTypes J).inverse.obj Y)).val ≫
        𝟙 (sheafify J (Y.val ⋙ G) ⋙ forget D) =
    (Adjunction.whiskerRight Cᵒᵖ adj).unit.app Y.val ≫ whiskerRight (toSheafify J (Y.val ⋙ G)) (forget D)
C : Type u
inst✝⁹ : Category C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category D
E : Type w₂
inst✝⁷ : Category E
F : D ⥤ E
G✝ : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
G : Type (max v u) ⥤ D
adj : G ⊣ forget D
Y : SheafOfTypes J
⊢ ((adjunctionToTypes J adj).unit.app Y).val =
    (Adjunction.whiskerRight Cᵒᵖ adj).unit.app ((sheafOfTypesToPresheaf J).obj Y) ≫
      whiskerRight
        (toSheafify J (((whiskeringRight Cᵒᵖ (Type (max v u)) D).obj G).obj ((sheafOfTypesToPresheaf J).obj Y)))
        (forget D)
dsimp [adjunctionToTypes, Adjunction.comp]
C : Type u
inst✝⁹ : Category C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category D
E : Type w₂
inst✝⁷ : Category E
F : D ⥤ E
G✝ : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
G : Type (max v u) ⥤ D
adj : G ⊣ forget D
Y : SheafOfTypes J
⊢ ((Equivalence.toAdjunction (Equivalence.symm (sheafEquivSheafOfTypes J))).unit.app Y).val ≫
      ↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) Y.val (sheafify J (Y.val ⋙ G)))
        (toSheafify J (Y.val ⋙ G)) =
    (Adjunction.whiskerRight Cᵒᵖ adj).unit.app Y.val ≫ whiskerRight (toSheafify J (Y.val ⋙ G)) (forget D)
C : Type u
inst✝⁹ : Category C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category D
E : Type w₂
inst✝⁷ : Category E
F : D ⥤ E
G✝ : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
G : Type (max v u) ⥤ D
adj : G ⊣ forget D
Y : SheafOfTypes J
⊢ ((Equivalence.toAdjunction (Equivalence.symm (sheafEquivSheafOfTypes J))).unit.app Y).val ≫
      ((adjunction J adj).unit.app ((sheafEquivSheafOfTypes J).inverse.obj Y)).val ≫
        𝟙 (sheafify J (Y.val ⋙ G) ⋙ forget D) =
    (Adjunction.whiskerRight Cᵒᵖ adj).unit.app Y.val ≫ whiskerRight (toSheafify J (Y.val ⋙ G)) (forget D)
simp
no goals
C : Type u
inst✝⁹ : Category C
J : GrothendieckTopology C
D : Type w₁
inst✝⁸ : Category D
E : Type w₂
inst✝⁷ : Category E
F : D ⥤ E
G✝ : E ⥤ D
inst✝⁶ : (X : C) → (S : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index S P)) F
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝² : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
G : Type (max v u) ⥤ D
adj : G ⊣ forget D
Y : SheafOfTypes J
⊢ ((Equivalence.toAdjunction (Equivalence.symm (sheafEquivSheafOfTypes J))).unit.app Y).val ≫
      ↑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) Y.val (sheafify J (Y.val ⋙ G)))
        (toSheafify J (Y.val ⋙ G)) =
    (Adjunction.whiskerRight Cᵒᵖ adj).unit.app Y.val ≫ whiskerRight (toSheafify J (Y.val ⋙ G)) (forget D)
rfl