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