F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : F α → α
x : F (Fix F)
this : recF g ∘ fixToW = rec g
⊢ rec g (mk x) = g (rec g <$> x)
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : F α → α
x : F (Fix F)
⊢ rec g (mk x) = g (rec g <$> x)
have : recF g ∘ fixToW = Fix.rec g := by
  apply funext
  apply Quotient.ind
  intro x
  apply recF_eq_of_Wequiv
  rw [fixToW]
  apply Wrepr_equiv
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : F α → α
x : F (Fix F)
this : recF g ∘ fixToW = rec g
⊢ recF g (PFunctor.W.mk (fixToW <$> repr x)) = g (rec g <$> x)
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : F α → α
x : F (Fix F)
this : recF g ∘ fixToW = rec g
⊢ rec g (mk x) = g (rec g <$> x)
conv =>
  lhs
  rw [Fix.rec, Fix.mk]
  dsimp
case mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : F α → α
x : F (Fix F)
this : recF g ∘ fixToW = rec g
a : (P F).A
f : PFunctor.B (P F) a → Fix F
h : repr x = { fst := a, snd := f }
⊢ recF g (PFunctor.W.mk (fixToW <$> { fst := a, snd := f })) = g (rec g <$> x)
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : F α → α
x : F (Fix F)
this : recF g ∘ fixToW = rec g
⊢ recF g (PFunctor.W.mk (fixToW <$> repr x)) = g (rec g <$> x)
cases' h : repr x with a f
no goals
case mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : F α → α
x : F (Fix F)
this : recF g ∘ fixToW = rec g
a : (P F).A
f : PFunctor.B (P F) a → Fix F
h : repr x = { fst := a, snd := f }
⊢ recF g (PFunctor.W.mk (fixToW <$> { fst := a, snd := f })) = g (rec g <$> x)
rw [PFunctor.map_eq, recF_eq, ← PFunctor.map_eq, PFunctor.W.dest_mk, ← PFunctor.comp_map, abs_map,
  ← h, abs_repr, this]
case h
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : F α → α
x : F (Fix F)
⊢ ∀ (x : Fix F), (recF g ∘ fixToW) x = rec g x
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : F α → α
x : F (Fix F)
⊢ recF g ∘ fixToW = rec g
apply funext
case h.a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : F α → α
x : F (Fix F)
⊢ ∀ (a : PFunctor.W (P F)), (recF g ∘ fixToW) (Quotient.mk Wsetoid a) = rec g (Quotient.mk Wsetoid a)
case h
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : F α → α
x : F (Fix F)
⊢ ∀ (x : Fix F), (recF g ∘ fixToW) x = rec g x
apply Quotient.ind
case h.a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : F α → α
x✝ : F (Fix F)
x : PFunctor.W (P F)
⊢ (recF g ∘ fixToW) (Quotient.mk Wsetoid x) = rec g (Quotient.mk Wsetoid x)
case h.a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : F α → α
x : F (Fix F)
⊢ ∀ (a : PFunctor.W (P F)), (recF g ∘ fixToW) (Quotient.mk Wsetoid a) = rec g (Quotient.mk Wsetoid a)
intro x
case h.a.a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : F α → α
x✝ : F (Fix F)
x : PFunctor.W (P F)
⊢ Wequiv (fixToW (Quotient.mk Wsetoid x)) x
case h.a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : F α → α
x✝ : F (Fix F)
x : PFunctor.W (P F)
⊢ (recF g ∘ fixToW) (Quotient.mk Wsetoid x) = rec g (Quotient.mk Wsetoid x)
apply recF_eq_of_Wequiv
case h.a.a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : F α → α
x✝ : F (Fix F)
x : PFunctor.W (P F)
⊢ Wequiv
    (Quotient.lift Wrepr
      (_ :
        ∀ (x y : PFunctor.W (P F)),
          Wequiv x y → recF (fun x => PFunctor.W.mk (repr x)) x = recF (fun x => PFunctor.W.mk (repr x)) y)
      (Quotient.mk Wsetoid x))
    x
case h.a.a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : F α → α
x✝ : F (Fix F)
x : PFunctor.W (P F)
⊢ Wequiv (fixToW (Quotient.mk Wsetoid x)) x
rw [fixToW]
no goals
case h.a.a
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
α : Type u
g : F α → α
x✝ : F (Fix F)
x : PFunctor.W (P F)
⊢ Wequiv
    (Quotient.lift Wrepr
      (_ :
        ∀ (x y : PFunctor.W (P F)),
          Wequiv x y → recF (fun x => PFunctor.W.mk (repr x)) x = recF (fun x => PFunctor.W.mk (repr x)) y)
      (Quotient.mk Wsetoid x))
    x
apply Wrepr_equiv