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
ih : ∀ (a : PFunctor.B (P F) a), Wequiv (Wrepr (f a)) (f a)
⊢ Wequiv (Wrepr (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 (Wrepr x) x
induction' x with a f ih
case 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
ih : ∀ (a : PFunctor.B (P F) a), Wequiv (Wrepr (f a)) (f a)
⊢ Wequiv (Wrepr (WType.mk a f)) ?mk.v

case 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
ih : ∀ (a : PFunctor.B (P F) a), Wequiv (Wrepr (f a)) (f a)
⊢ Wequiv ?mk.v (WType.mk a f)

case mk.v
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
ih : ∀ (a : PFunctor.B (P F) a), Wequiv (Wrepr (f a)) (f a)
⊢ PFunctor.W (P F)
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
ih : ∀ (a : PFunctor.B (P F) a), Wequiv (Wrepr (f a)) (f a)
⊢ Wequiv (Wrepr (WType.mk a f)) (WType.mk a f)
apply Wequiv.trans
case mk.a.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
ih : ∀ (a : PFunctor.B (P F) a), Wequiv (Wrepr (f a)) (f a)
⊢ ∀ (x : PFunctor.B (P F) a), Wequiv ((Wrepr ∘ f) x) (f x)
case 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
ih : ∀ (a : PFunctor.B (P F) a), Wequiv (Wrepr (f a)) (f a)
⊢ Wequiv (PFunctor.W.mk (Wrepr <$> { fst := a, snd := f })) (WType.mk a f)
apply Wequiv.ind
no goals
case mk.a.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
ih : ∀ (a : PFunctor.B (P F) a), Wequiv (Wrepr (f a)) (f a)
⊢ ∀ (x : PFunctor.B (P F) a), Wequiv ((Wrepr ∘ f) x) (f x)
exact ih
case 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
ih : ∀ (a : PFunctor.B (P F) a), Wequiv (Wrepr (f a)) (f a)
⊢ Wequiv (Wrepr (WType.mk a f)) (PFunctor.W.mk (Wrepr <$> { fst := a, snd := f }))
case 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
ih : ∀ (a : PFunctor.B (P F) a), Wequiv (Wrepr (f a)) (f a)
⊢ Wequiv (Wrepr (WType.mk a f)) ?mk.v
change Wequiv (Wrepr ⟨a, f⟩) (PFunctor.W.mk (Wrepr <$> ⟨a, f⟩))
case mk.a.h
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
ih : ∀ (a : PFunctor.B (P F) a), Wequiv (Wrepr (f a)) (f a)
⊢ abs (PFunctor.W.dest (Wrepr (WType.mk a f))) =
    abs (PFunctor.W.dest (PFunctor.W.mk (Wrepr <$> { fst := a, snd := f })))
case 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
ih : ∀ (a : PFunctor.B (P F) a), Wequiv (Wrepr (f a)) (f a)
⊢ Wequiv (Wrepr (WType.mk a f)) (PFunctor.W.mk (Wrepr <$> { fst := a, snd := f }))
apply Wequiv.abs'
case mk.a.h
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
ih : ∀ (a : PFunctor.B (P F) a), Wequiv (Wrepr (f a)) (f a)
this : Wrepr (WType.mk a f) = PFunctor.W.mk (repr (abs (Wrepr <$> { fst := a, snd := f })))
⊢ abs (PFunctor.W.dest (Wrepr (WType.mk a f))) =
    abs (PFunctor.W.dest (PFunctor.W.mk (Wrepr <$> { fst := a, snd := f })))
case mk.a.h
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
ih : ∀ (a : PFunctor.B (P F) a), Wequiv (Wrepr (f a)) (f a)
⊢ abs (PFunctor.W.dest (Wrepr (WType.mk a f))) =
    abs (PFunctor.W.dest (PFunctor.W.mk (Wrepr <$> { fst := a, snd := f })))
have : Wrepr ⟨a, f⟩ = PFunctor.W.mk (repr (abs (Wrepr <$> ⟨a, f⟩))) := rfl
case mk.a.h
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
ih : ∀ (a : PFunctor.B (P F) a), Wequiv (Wrepr (f a)) (f a)
this : Wrepr (WType.mk a f) = PFunctor.W.mk (repr (abs (Wrepr <$> { fst := a, snd := f })))
⊢ abs (Wrepr <$> { fst := a, snd := f }) = abs (PFunctor.W.dest (PFunctor.W.mk (Wrepr <$> { fst := a, snd := f })))
case mk.a.h
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
ih : ∀ (a : PFunctor.B (P F) a), Wequiv (Wrepr (f a)) (f a)
this : Wrepr (WType.mk a f) = PFunctor.W.mk (repr (abs (Wrepr <$> { fst := a, snd := f })))
⊢ abs (PFunctor.W.dest (Wrepr (WType.mk a f))) =
    abs (PFunctor.W.dest (PFunctor.W.mk (Wrepr <$> { fst := a, snd := f })))
rw [this, PFunctor.W.dest_mk, abs_repr]
no goals
case mk.a.h
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
ih : ∀ (a : PFunctor.B (P F) a), Wequiv (Wrepr (f a)) (f a)
this : Wrepr (WType.mk a f) = PFunctor.W.mk (repr (abs (Wrepr <$> { fst := a, snd := f })))
⊢ abs (Wrepr <$> { fst := a, snd := f }) = abs (PFunctor.W.dest (PFunctor.W.mk (Wrepr <$> { fst := a, snd := f })))
rfl