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 β
g : α → F β
h : β → G γ
x✝ : t α
⊢ traverse (Comp.mk ∘ map h ∘ g) x✝ = (Comp.mk ∘ map (traverse h) ∘ traverse g) 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 β
g : α → F β
h : β → G γ
⊢ traverse (Comp.mk ∘ map h ∘ g) = Comp.mk ∘ map (traverse h) ∘ traverse g
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 β
g : α → F β
h : β → G γ
x✝ : t α
⊢ traverse (Comp.mk ∘ map h ∘ g) x✝ = (Comp.mk ∘ map (traverse h) ∘ traverse g) x✝
exact comp_traverse _ _ _