Traversable and Option

Stream: mathlib4

[Harry Goldstein]

Hi all, I'm trying to prove this theorem about the way Traversables interact with Options, and I'm stuck on both directions:

theorem sequence_some
    {γ : Type}
    {F : Type → Type}
    [Functor F]
    [Traversable F]
    [LawfulTraversable F]
    (t : F (Option γ))
    (t' : F γ) :
    sequence t = Option.some t' ↔ t = Option.some <$> t' := by
  apply Iff.intro
  . intro h
    /-
    case mp
    ...
    h : sequence t = some t'
    ⊢ t = some <$> t'
    NOTE: Might not be true?
    -/
    sorry
  . intro h
    subst h
    rw [Eq.comm]
    /-
    case mpr
    ...
    ⊢ some t' = sequence (some <$> t')
    NOTE: Should follow by naturality?
    -/
    sorry

The right to left direction is really the one I'm asking for help with: I know it should follow from naturality, but I can't seem to get the types to line up. Does someone have a minute to help me wrangle the implicits?

The left to right direction I'm actually not sure is true, but if anyone has an idea for how to prove that I'd also really appreciate it.

[Notification Bot]

Harry Goldstein has marked this topic as resolved.

[Eric Wieser]

This is surely false without LawfulFunctor?

[Notification Bot]

Harry Goldstein has marked this topic as unresolved.

[Harry Goldstein]

I believe LawfulTraversable depends on LawfulFunctor, no?

[Eric Wieser]

Ah, in that case you should remove Functor, since otherwise you're assuming two unrelated functor structures