case mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
a : (P F).A
f : PFunctor.B (P F) a → WType (P F).B
⊢ Wequiv (WType.mk a f) (WType.mk a f)
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x : PFunctor.W (P F)
⊢ Wequiv x x
cases' x with a f
no goals
case mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
a : (P F).A
f : PFunctor.B (P F) a → WType (P F).B
⊢ Wequiv (WType.mk a f) (WType.mk a f)
exact Wequiv.abs a f a f rfl