## Stream: general

### Topic: error after completing tactic proof

#### Johan Commelin (Nov 17 2018 at 06:37):

type mismatch at application
F.map (i ≫ functor.preimage f j) s
term
s
has type
((functor.id (presheaf X)).obj F_1).obj U₁_1
but is expected to have type
F.obj U₁
types contain aliased name(s): U₁ F
remark: the tactic dedup can be used to rename aliases


I have tried inserting dedup in several places, but it doesn't help. My s remains to have type ((functor.id (presheaf X)).obj F).obj U₁ in the goal window, which is defeq to F.obj U₁.

#### Scott Morrison (Nov 17 2018 at 07:14):

Oh, I've had this one before. The error message is completely misleading...

#### Scott Morrison (Nov 17 2018 at 07:15):

Check that you haven't somehow used _root_.functor somewhere that should have been category_theory.functor?

#### Scott Morrison (Nov 17 2018 at 07:15):

I don't remember if that was it or not.

#### Johan Commelin (Nov 17 2018 at 07:40):

Hmm, that sounds like a very crazy error. I'll see if I can find it.

#### Johan Commelin (Nov 17 2018 at 07:42):

Do you spot anything suspicious in

def counit.is_iso [fully_faithful f] : is_iso (counit f) :=
{ inv :=
{ app := λ (F : _ ⥤ _),
{ app := λ U s,
{ app := λ V i, (F.map $f.preimage i : F.obj U → F.obj V) s, naturality' := λ V₁ V₂ i, begin ext j, have := (congr$ F.map_comp (f.preimage j) i) (rfl : s = _),
dsimp at *,
erw ← this,
congr,
apply f.injectivity,
erw f.map_comp,
tidy {trace_result := tt},
end },
naturality' := λ U₁ U₂ i,
begin
ext s V j,
have := (congr $F.map_comp i (f.preimage j)) (rfl : _ = _), dsimp at *, erw ← this, congr, apply f.injectivity, erw f.map_comp, tidy {trace_result := tt}, end }, naturality' := λ F G α, begin ext U s V j, have := (congr$ α.naturality (f.op.preimage j)) rfl,
tidy {trace_result := tt},
end } }


#### Johan Commelin (Nov 17 2018 at 10:31):

@Scott Morrison In my case it was talking about f.preimage while that should have been f.op.preimage.
I think we should have stronger barriers between categories and their opposites. Because now stuff is silently identified, and then all of a sudden it bites you 20 lines later.

#### Johan Commelin (Nov 17 2018 at 10:57):

Hmm, no, that wasn't the issue... it reappeared...

#### Johan Commelin (Nov 17 2018 at 11:02):

I pushed an update to the sheaf branch. The trouble is with this def: https://github.com/leanprover-community/mathlib/blob/sheaf/category_theory/sheaf.lean#L241
If any of the experts would want to take a look, I would be very grateful.

Last updated: May 10 2021 at 00:31 UTC