case mk
P : PFunctor
α β : Type u
fst✝ : P.A
snd✝ : B P fst✝ → W P
⊢ dest (mk { fst := fst✝, snd := snd✝ }) = { fst := fst✝, snd := snd✝ }
P : PFunctor
α β : Type u
p : Obj P (W P)
⊢ dest (mk p) = p
cases p
no goals
case mk
P : PFunctor
α β : Type u
fst✝ : P.A
snd✝ : B P fst✝ → W P
⊢ dest (mk { fst := fst✝, snd := snd✝ }) = { fst := fst✝, snd := snd✝ }
rfl