case h
F : Type u → Type v
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
G : Type u → Type w
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α β : Type u
x : α → β
y : F α
⊢ ((fun {α} => app η α) ∘ Functor.map x) y = (Functor.map x ∘ fun {α} => app η α) y
F : Type u → Type v
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
G : Type u → Type w
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α β : Type u
x : α → β
⊢ (fun {α} => app η α) ∘ Functor.map x = Functor.map x ∘ fun {α} => app η α
ext y
no goals
case h
F : Type u → Type v
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
G : Type u → Type w
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α β : Type u
x : α → β
y : F α
⊢ ((fun {α} => app η α) ∘ Functor.map x) y = (Functor.map x ∘ fun {α} => app η α) y
exact preserves_map η x y