F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x y : PFunctor.W (P F)
h : Wequiv x y
⊢ Wequiv y x
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x y : PFunctor.W (P F)
⊢ Wequiv x y → Wequiv y x
intro h
case ind
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x y : PFunctor.W (P F)
a✝¹ : (P F).A
f✝ f'✝ : PFunctor.B (P F) a✝¹ → PFunctor.W (P F)
a✝ : ∀ (x : PFunctor.B (P F) a✝¹), Wequiv (f✝ x) (f'✝ x)
a_ih✝ : ∀ (x : PFunctor.B (P F) a✝¹), Wequiv (f'✝ x) (f✝ x)
⊢ Wequiv (WType.mk a✝¹ f'✝) (WType.mk a✝¹ f✝)

case abs
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x y : PFunctor.W (P F)
a✝¹ : (P F).A
f✝ : PFunctor.B (P F) a✝¹ → PFunctor.W (P F)
a'✝ : (P F).A
f'✝ : PFunctor.B (P F) a'✝ → PFunctor.W (P F)
a✝ : Qpf.abs { fst := a✝¹, snd := f✝ } = Qpf.abs { fst := a'✝, snd := f'✝ }
⊢ Wequiv (WType.mk a'✝ f'✝) (WType.mk a✝¹ f✝)

case trans
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x y u✝ v✝ w✝ : PFunctor.W (P F)
a✝¹ : Wequiv u✝ v✝
a✝ : Wequiv v✝ w✝
a_ih✝¹ : Wequiv v✝ u✝
a_ih✝ : Wequiv w✝ v✝
⊢ Wequiv w✝ u✝
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x y : PFunctor.W (P F)
h : Wequiv x y
⊢ Wequiv y x
induction h
case abs
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x y : PFunctor.W (P F)
a✝¹ : (P F).A
f✝ : PFunctor.B (P F) a✝¹ → PFunctor.W (P F)
a'✝ : (P F).A
f'✝ : PFunctor.B (P F) a'✝ → PFunctor.W (P F)
a✝ : Qpf.abs { fst := a✝¹, snd := f✝ } = Qpf.abs { fst := a'✝, snd := f'✝ }
⊢ Wequiv (WType.mk a'✝ f'✝) (WType.mk a✝¹ f✝)

case trans
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x y u✝ v✝ w✝ : PFunctor.W (P F)
a✝¹ : Wequiv u✝ v✝
a✝ : Wequiv v✝ w✝
a_ih✝¹ : Wequiv v✝ u✝
a_ih✝ : Wequiv w✝ v✝
⊢ Wequiv w✝ u✝
case ind
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x y : PFunctor.W (P F)
a✝¹ : (P F).A
f✝ f'✝ : PFunctor.B (P F) a✝¹ → PFunctor.W (P F)
a✝ : ∀ (x : PFunctor.B (P F) a✝¹), Wequiv (f✝ x) (f'✝ x)
a_ih✝ : ∀ (x : PFunctor.B (P F) a✝¹), Wequiv (f'✝ x) (f✝ x)
⊢ Wequiv (WType.mk a✝¹ f'✝) (WType.mk a✝¹ f✝)

case abs
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x y : PFunctor.W (P F)
a✝¹ : (P F).A
f✝ : PFunctor.B (P F) a✝¹ → PFunctor.W (P F)
a'✝ : (P F).A
f'✝ : PFunctor.B (P F) a'✝ → PFunctor.W (P F)
a✝ : Qpf.abs { fst := a✝¹, snd := f✝ } = Qpf.abs { fst := a'✝, snd := f'✝ }
⊢ Wequiv (WType.mk a'✝ f'✝) (WType.mk a✝¹ f✝)

case trans
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x y u✝ v✝ w✝ : PFunctor.W (P F)
a✝¹ : Wequiv u✝ v✝
a✝ : Wequiv v✝ w✝
a_ih✝¹ : Wequiv v✝ u✝
a_ih✝ : Wequiv w✝ v✝
⊢ Wequiv w✝ u✝
case ind a f f' _ ih => exact Wequiv.ind _ _ _ ih
case trans
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x y u✝ v✝ w✝ : PFunctor.W (P F)
a✝¹ : Wequiv u✝ v✝
a✝ : Wequiv v✝ w✝
a_ih✝¹ : Wequiv v✝ u✝
a_ih✝ : Wequiv w✝ v✝
⊢ Wequiv w✝ u✝
case abs
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x y : PFunctor.W (P F)
a✝¹ : (P F).A
f✝ : PFunctor.B (P F) a✝¹ → PFunctor.W (P F)
a'✝ : (P F).A
f'✝ : PFunctor.B (P F) a'✝ → PFunctor.W (P F)
a✝ : Qpf.abs { fst := a✝¹, snd := f✝ } = Qpf.abs { fst := a'✝, snd := f'✝ }
⊢ Wequiv (WType.mk a'✝ f'✝) (WType.mk a✝¹ f✝)

case trans
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x y u✝ v✝ w✝ : PFunctor.W (P F)
a✝¹ : Wequiv u✝ v✝
a✝ : Wequiv v✝ w✝
a_ih✝¹ : Wequiv v✝ u✝
a_ih✝ : Wequiv w✝ v✝
⊢ Wequiv w✝ u✝
case abs a f a' f' h => exact Wequiv.abs _ _ _ _ h.symm
no goals
case trans
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x y u✝ v✝ w✝ : PFunctor.W (P F)
a✝¹ : Wequiv u✝ v✝
a✝ : Wequiv v✝ w✝
a_ih✝¹ : Wequiv v✝ u✝
a_ih✝ : Wequiv w✝ v✝
⊢ Wequiv w✝ u✝
case trans x y z _ _ ih₁ ih₂ => exact Qpf.Wequiv.trans _ _ _ ih₂ ih₁
no goals
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x y : PFunctor.W (P F)
a : (P F).A
f f' : PFunctor.B (P F) a → PFunctor.W (P F)
a✝ : ∀ (x : PFunctor.B (P F) a), Wequiv (f x) (f' x)
ih : ∀ (x : PFunctor.B (P F) a), Wequiv (f' x) (f x)
⊢ Wequiv (WType.mk a f') (WType.mk a f)
exact Wequiv.ind _ _ _ ih
no goals
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x y : PFunctor.W (P F)
a : (P F).A
f : PFunctor.B (P F) a → PFunctor.W (P F)
a' : (P F).A
f' : PFunctor.B (P F) a' → PFunctor.W (P F)
h : Qpf.abs { fst := a, snd := f } = Qpf.abs { fst := a', snd := f' }
⊢ Wequiv (WType.mk a' f') (WType.mk a f)
exact Wequiv.abs _ _ _ _ h.symm
no goals
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x✝ y✝ x y z : PFunctor.W (P F)
a✝¹ : Wequiv x y
a✝ : Wequiv y z
ih₁ : Wequiv y x
ih₂ : Wequiv z y
⊢ Wequiv z x
exact Qpf.Wequiv.trans _ _ _ ih₂ ih₁