C : Type u
inst✝ : Category C
X : TopCat
ℱ : Presheaf C X
U : Set ↑X
p : IsOpen U
⊢ (whiskerRight (NatTrans.op (Opens.mapId X).inv) ℱ ≫ (Functor.leftUnitor ℱ).hom).app
      { carrier := U, is_open' := p }.op =
    ℱ.map (𝟙 { carrier := U, is_open' := p }.op)
C : Type u
inst✝ : Category C
X : TopCat
ℱ : Presheaf C X
U : Set ↑X
p : IsOpen U
⊢ (id ℱ).hom.app { carrier := U, is_open' := p }.op = ℱ.map (𝟙 { carrier := U, is_open' := p }.op)
dsimp [id]
no goals
C : Type u
inst✝ : Category C
X : TopCat
ℱ : Presheaf C X
U : Set ↑X
p : IsOpen U
⊢ (whiskerRight (NatTrans.op (Opens.mapId X).inv) ℱ ≫ (Functor.leftUnitor ℱ).hom).app
      { carrier := U, is_open' := p }.op =
    ℱ.map (𝟙 { carrier := U, is_open' := p }.op)
simp [CategoryStruct.comp]