t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁵ : Traversable t
inst✝⁴ : IsLawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α β γ : Type u
f : β → F γ
g : α → G β
x : t' α
⊢ Comp.mk (((fun x => ↑(eqv γ) <$> x) ∘ traverse f) <$> traverse g (↑(eqv α).symm x)) =
    Comp.mk (((fun x => ↑(eqv γ) <$> traverse f (↑(eqv β).symm x)) ∘ ↑(eqv β)) <$> traverse g (↑(eqv α).symm x))
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁵ : Traversable t
inst✝⁴ : IsLawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α β γ : Type u
f : β → F γ
g : α → G β
x : t' α
⊢ Equiv.traverse eqv (Comp.mk ∘ map f ∘ g) x = Comp.mk (Equiv.traverse eqv f <$> Equiv.traverse eqv g x)
simp [Equiv.traverse, comp_traverse, functor_norm]
case e_x.e_a
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁵ : Traversable t
inst✝⁴ : IsLawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α β γ : Type u
f : β → F γ
g : α → G β
x : t' α
⊢ (fun x => ↑(eqv γ) <$> x) ∘ traverse f = (fun x => ↑(eqv γ) <$> traverse f (↑(eqv β).symm x)) ∘ ↑(eqv β)
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁵ : Traversable t
inst✝⁴ : IsLawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α β γ : Type u
f : β → F γ
g : α → G β
x : t' α
⊢ Comp.mk (((fun x => ↑(eqv γ) <$> x) ∘ traverse f) <$> traverse g (↑(eqv α).symm x)) =
    Comp.mk (((fun x => ↑(eqv γ) <$> traverse f (↑(eqv β).symm x)) ∘ ↑(eqv β)) <$> traverse g (↑(eqv α).symm x))
congr
case e_x.e_a.h
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁵ : Traversable t
inst✝⁴ : IsLawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α β γ : Type u
f : β → F γ
g : α → G β
x : t' α
x✝ : t β
⊢ ((fun x => ↑(eqv γ) <$> x) ∘ traverse f) x✝ = ((fun x => ↑(eqv γ) <$> traverse f (↑(eqv β).symm x)) ∘ ↑(eqv β)) x✝
case e_x.e_a
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁵ : Traversable t
inst✝⁴ : IsLawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α β γ : Type u
f : β → F γ
g : α → G β
x : t' α
⊢ (fun x => ↑(eqv γ) <$> x) ∘ traverse f = (fun x => ↑(eqv γ) <$> traverse f (↑(eqv β).symm x)) ∘ ↑(eqv β)
ext
no goals
case e_x.e_a.h
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁵ : Traversable t
inst✝⁴ : IsLawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α β γ : Type u
f : β → F γ
g : α → G β
x : t' α
x✝ : t β
⊢ ((fun x => ↑(eqv γ) <$> x) ∘ traverse f) x✝ = ((fun x => ↑(eqv γ) <$> traverse f (↑(eqv β).symm x)) ∘ ↑(eqv β)) x✝
simp