Lean4
theorem ext {F} :
∀ {A1 : Applicative F} {A2 : Applicative F} [@LawfulApplicative F A1] [@LawfulApplicative F A2],
(∀ {α : Type u} (x : α), @Pure.pure _ A1.toPure _ x = @Pure.pure _ A2.toPure _ x) →
(∀ {α β : Type u} (f : F (α → β)) (x : F α),
@Seq.seq _ A1.toSeq _ _ f (fun _ => x) = @Seq.seq _ A2.toSeq _ _ f (fun _ => x)) →
A1 = A2
| { toFunctor := F1, seq := s1, pure := p1, seqLeft := sl1, seqRight := sr1 },
{ toFunctor := F2, seq := s2, pure := p2, seqLeft := sl2, seqRight := sr2 }, L1, L2, H1, H2 =>
by
obtain rfl : @p1 = @p2 := by
funext α x
apply H1
obtain rfl : @s1 = @s2 := by
funext α β f x
exact H2 f (x Unit.unit)
obtain ⟨seqLeft_eq1, seqRight_eq1, pure_seq1, -⟩ := L1
obtain ⟨seqLeft_eq2, seqRight_eq2, pure_seq2, -⟩ := L2
obtain rfl : F1 = F2 := by
apply Functor.ext
intros
exact (pure_seq1 _ _).symm.trans (pure_seq2 _ _)
congr <;> funext α β x y
· exact (seqLeft_eq1 _ (y Unit.unit)).trans (seqLeft_eq2 _ _).symm
· exact (seqRight_eq1 _ (y Unit.unit)).trans (seqRight_eq2 _ (y Unit.unit)).symm
