unfold map
α : Sort u_1
β γ δ : Type u_2
f : α ⇀ β
g₁ : β → γ
g₂ : γ → δ
⊢ map g₂ (map g₁ f) = map (g₂ ∘ g₁) f
α : Sort u_1
β γ δ : Type u_2
f : α ⇀ β
g₁ : β → γ
g₂ : γ → δ
⊢ (fun a => g₂ <$> g₁ <$> f a) = fun a => (g₂ ∘ g₁) <$> f a