F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α β γ : Type u
f : α → β
g : β → γ
x : F α
⊢ (g ∘ f) <$> abs (repr x) = g <$> f <$> abs (repr x)
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α β γ : Type u
f : α → β
g : β → γ
x : F α
⊢ (g ∘ f) <$> x = g <$> f <$> x
rw [← abs_repr x]
case mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α β γ : Type u
f✝ : α → β
g : β → γ
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
⊢ (g ∘ f✝) <$> abs { fst := a, snd := f } = g <$> f✝ <$> abs { fst := a, snd := f }
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α β γ : Type u
f : α → β
g : β → γ
x : F α
⊢ (g ∘ f) <$> abs (repr x) = g <$> f <$> abs (repr x)
cases' repr x with a f
case mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α β γ : Type u
f✝ : α → β
g : β → γ
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
⊢ abs ((g ∘ f✝) <$> { fst := a, snd := f }) = abs (g <$> f✝ <$> { fst := a, snd := f })
case mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α β γ : Type u
f✝ : α → β
g : β → γ
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
⊢ (g ∘ f✝) <$> abs { fst := a, snd := f } = g <$> f✝ <$> abs { fst := a, snd := f }
rw [← abs_map, ← abs_map, ← abs_map]
no goals
case mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α β γ : Type u
f✝ : α → β
g : β → γ
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
⊢ abs ((g ∘ f✝) <$> { fst := a, snd := f }) = abs (g <$> f✝ <$> { fst := a, snd := f })
rfl