case h
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj PUnit.op
x : α
⊢ eval S α (typesGlue S hs α f) x = f x
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj PUnit.op
⊢ eval S α (typesGlue S hs α f) = f
funext x
case h
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj PUnit.op
x : α
⊢ S.map (↾fun x => PUnit.unit).op (f ((↾fun x_1 => x) (Classical.choose (_ : ∃ x, ∀ (y : PUnit), y = x)))) = f x
case h
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj PUnit.op
x : α
⊢ eval S α (typesGlue S hs α f) x = f x
apply (IsSheafFor.valid_glue _ _ _ <| ⟨PUnit.unit, fun _ => Subsingleton.elim _ _⟩).trans
no goals
case h
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj PUnit.op
x : α
⊢ S.map (↾fun x => PUnit.unit).op (f ((↾fun x_1 => x) (Classical.choose (_ : ∃ x, ∀ (y : PUnit), y = x)))) = f x
convert FunctorToTypes.map_id_apply S _