case mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
y : PFunctor.W (P F)
a✝ : (P F).A
f✝ : PFunctor.B (P F) a✝ → WType (P F).B
h : Qpf.abs (PFunctor.W.dest (WType.mk a✝ f✝)) = Qpf.abs (PFunctor.W.dest y)
⊢ Wequiv (WType.mk a✝ f✝) y
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x y : PFunctor.W (P F)
h : Qpf.abs (PFunctor.W.dest x) = Qpf.abs (PFunctor.W.dest y)
⊢ Wequiv x y
cases x
case mk.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
a✝ : (P F).A
f✝ : PFunctor.B (P F) a✝ → WType (P F).B
h : Qpf.abs (PFunctor.W.dest (WType.mk a✝¹ f✝¹)) = Qpf.abs (PFunctor.W.dest (WType.mk a✝ f✝))
⊢ Wequiv (WType.mk a✝¹ f✝¹) (WType.mk a✝ f✝)
case mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
y : PFunctor.W (P F)
a✝ : (P F).A
f✝ : PFunctor.B (P F) a✝ → WType (P F).B
h : Qpf.abs (PFunctor.W.dest (WType.mk a✝ f✝)) = Qpf.abs (PFunctor.W.dest y)
⊢ Wequiv (WType.mk a✝ f✝) y
cases y
case mk.mk.a
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
a✝ : (P F).A
f✝ : PFunctor.B (P F) a✝ → WType (P F).B
h : Qpf.abs (PFunctor.W.dest (WType.mk a✝¹ f✝¹)) = Qpf.abs (PFunctor.W.dest (WType.mk a✝ f✝))
⊢ Qpf.abs { fst := a✝¹, snd := f✝¹ } = Qpf.abs { fst := a✝, snd := f✝ }
case mk.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
a✝ : (P F).A
f✝ : PFunctor.B (P F) a✝ → WType (P F).B
h : Qpf.abs (PFunctor.W.dest (WType.mk a✝¹ f✝¹)) = Qpf.abs (PFunctor.W.dest (WType.mk a✝ f✝))
⊢ Wequiv (WType.mk a✝¹ f✝¹) (WType.mk a✝ f✝)
apply Wequiv.abs
no goals
case mk.mk.a
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
a✝ : (P F).A
f✝ : PFunctor.B (P F) a✝ → WType (P F).B
h : Qpf.abs (PFunctor.W.dest (WType.mk a✝¹ f✝¹)) = Qpf.abs (PFunctor.W.dest (WType.mk a✝ f✝))
⊢ Qpf.abs { fst := a✝¹, snd := f✝¹ } = Qpf.abs { fst := a✝, snd := f✝ }
apply h