Applicative composition is too hard 😿

Changes

1 changed files (+39/-1)

• Category.lean
  • @@ -274,4 +274,42 @@ theorem coyoneda_lemma' (y : f α) [Cofunctor f] : coyoneda (coyoneda' y) = y :=
    simp [coyoneda, coyoneda', Cofunctor.id_comap] - -- TODO: Applicatives, monads, Kleisi categories + -- TODO: Applicatives + #check Applicative + #check LawfulApplicative + + /-- Composition of two applicatives is an applicative -/ + @[simp] + instance [Applicative f] [LawfulApplicative f] [Applicative g] [LawfulApplicative g] : Applicative (f ∘ g) where + pure x := pure (f := f) (pure x) + seq h x := Seq.seq (f := f) ((· <*> ·) <$> h) x + + 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] + 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] + + + -- TODO: Monads + #check Monad + #check LawfulMonad + + /- + Sadly, in general monads do not compose 😿 + However, in some cases we can use monad transformers to compose them + https://carlo-hamalainen.net/2014/01/02/applicatives-compose-monads-do-not/ + -/ + + -- TODO: Kleisi categories