Lean4
/-- `yoneda'` induces an equivalence of category between `Type u` and
`Sheaf typesGrothendieckTopology (Type u)`. -/
@[simps!]
noncomputable def typeEquiv : Type u ≌ Sheaf typesGrothendieckTopology (Type u)
where
functor := yoneda'
inverse := sheafToPresheaf _ _ ⋙ (evaluation _ _).obj (op PUnit)
unitIso :=
NatIso.ofComponents
(fun _α => -- α ≅ PUnit ⟶ α
{ hom := fun x _ => x
inv := fun f => f PUnit.unit
hom_inv_id := funext fun _ => rfl
inv_hom_id := funext fun _ => funext fun y => PUnit.casesOn y rfl })
fun _ => rfl
counitIso :=
Iso.symm <|
NatIso.ofComponents (fun S => equivYoneda' S)
(fun {S₁ S₂} f => by
ext ⟨α⟩ s
dsimp at s ⊢
ext x
exact eval_app S₁ S₂ f α s x)
functor_unitIso_comp
X := by
ext1
apply yonedaEquiv.injective
dsimp [yoneda', yonedaEquiv, evalEquiv]
erw [typesGlue_eval]
