case mk
P : PFunctor
α✝ β✝ α β : Type u
f : α → β
fst✝ : P.A
snd✝ : B P fst✝ → α
⊢ (f <$> { fst := fst✝, snd := snd✝ }).fst = { fst := fst✝, snd := snd✝ }.fst
P : PFunctor
α✝ β✝ α β : Type u
x : Obj P α
f : α → β
⊢ (f <$> x).fst = x.fst
cases x
no goals
case mk
P : PFunctor
α✝ β✝ α β : Type u
f : α → β
fst✝ : P.A
snd✝ : B P fst✝ → α
⊢ (f <$> { fst := fst✝, snd := snd✝ }).fst = { fst := fst✝, snd := snd✝ }.fst
rfl