Composition of applicatives proof yay

Changes

1 changed files (+6/-12)

• Category.lean
  • @@ -287,20 +287,14 @@ instance [Applicative f] [LawfulApplicative f] [Applicative g] [LawfulApplicativ
    instance [Applicative f] [LawfulApplicative f] [Applicative g] [LawfulApplicative g] : LawfulApplicative (f ∘ g) where seqLeft_eq := by simp seqRight_eq := by simp - pure_seq := by simp [LawfulApplicative.pure_seq] + pure_seq := by simp [pure_seq] map_pure := by simp seq_pure := by simp seq_assoc x h h' := by - sorry - -- simp - -- rw [LawfulApplicative.seq_assoc] - -- suffices Function.comp <$> (fun x1 x2 ↦ x1 <*> x2) <$> h' <*> (fun x1 x2 ↦ x1 <*> x2) <$> h = (fun x1 x2 ↦ x1 <*> x2) <$> ((fun a x2 ↦ Function.comp <$> a <*> x2) <$> h' <*> h) by grind - -- simp - -- rw [Functor.map_map] - -- rw [LawfulApplicative.seq_assoc] - - -- simp [LawfulApplicative.seq_assoc] - + simp [seq_assoc, seq_map_assoc, map_seq] + congr 3 + ext + simp [seq_assoc] -- TODO: Monads #check Monad
  • @@ -308,7 +302,7 @@ instance [Applicative f] [LawfulApplicative f] [Applicative g] [LawfulApplicativ
    /- Sadly, in general monads do not compose 😿 - However, in some cases we can use monad transformers to compose them + However, in some cases we can use monad transformers to compose them. https://carlo-hamalainen.net/2014/01/02/applicatives-compose-monads-do-not/ -/