case h
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : IsLawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
f : β → γ
x : t β
x✝ : t α
⊢ traverse pure x✝ = pure x✝
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : IsLawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
f : β → γ
x : t β
⊢ traverse pure = pure
ext
no goals
case h
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : IsLawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
f : β → γ
x : t β
x✝ : t α
⊢ traverse pure x✝ = pure x✝
exact id_traverse _