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
h : ∀ (α : Type u) (x : F α), (fun {α} => app η α) x = (fun {α} => app η' α) x
⊢ (fun {α} => app η α) = fun {α} => app η' α
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
h : ∀ (α : Type u) (x : F α), (fun {α} => app η α) x = (fun {α} => app η' α) x
⊢ η = η'
apply coe_inj
case h.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
h : ∀ (α : Type u) (x : F α), (fun {α} => app η α) x = (fun {α} => app η' α) x
α : Type u
⊢ app η α = app η' α
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
h : ∀ (α : Type u) (x : F α), (fun {α} => app η α) x = (fun {α} => app η' α) x
⊢ (fun {α} => app η α) = fun {α} => app η' α
ext1 α
no goals
case h.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
h : ∀ (α : Type u) (x : F α), (fun {α} => app η α) x = (fun {α} => app η' α) x
α : Type u
⊢ app η α = app η' α
exact funext (h α)