n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
this : recF g ∘ fixToW = rec g
⊢ rec g (mk x) = g ((TypeVec.id ::: rec g) <$$> x)
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
⊢ rec g (mk x) = g ((TypeVec.id ::: rec g) <$$> x)
have : recF g ∘ fixToW = Fix.rec g := by
  apply funext
  apply Quotient.ind
  intro x
  apply recF_eq_of_wEquiv
  apply wrepr_equiv
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
this : recF g ∘ fixToW = rec g
⊢ recF g (MvPFunctor.wMk' (P F) ((TypeVec.id ::: fixToW) <$$> repr x)) = g ((TypeVec.id ::: rec g) <$$> x)
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
this : recF g ∘ fixToW = rec g
⊢ rec g (mk x) = g ((TypeVec.id ::: rec g) <$$> x)
conv =>
  lhs
  rw [Fix.rec, Fix.mk]
  dsimp
case mk
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
this : recF g ∘ fixToW = rec g
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α ::: Fix F α
h : repr x = { fst := a, snd := f }
⊢ recF g (MvPFunctor.wMk' (P F) ((TypeVec.id ::: fixToW) <$$> { fst := a, snd := f })) =
    g ((TypeVec.id ::: rec g) <$$> x)
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
this : recF g ∘ fixToW = rec g
⊢ recF g (MvPFunctor.wMk' (P F) ((TypeVec.id ::: fixToW) <$$> repr x)) = g ((TypeVec.id ::: rec g) <$$> x)
cases' h : repr x with a f
case mk
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
this : recF g ∘ fixToW = rec g
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α ::: Fix F α
h : repr x = { fst := a, snd := f }
⊢ g (abs ((TypeVec.id ::: recF g) <$$> (TypeVec.id ::: fixToW) <$$> { fst := a, snd := f })) =
    g ((TypeVec.id ::: rec g) <$$> x)
case mk
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
this : recF g ∘ fixToW = rec g
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α ::: Fix F α
h : repr x = { fst := a, snd := f }
⊢ recF g (MvPFunctor.wMk' (P F) ((TypeVec.id ::: fixToW) <$$> { fst := a, snd := f })) =
    g ((TypeVec.id ::: rec g) <$$> x)
rw [MvPFunctor.map_eq, recF_eq', ← MvPFunctor.map_eq, MvPFunctor.wDest'_wMk']
no goals
case mk
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
this : recF g ∘ fixToW = rec g
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α ::: Fix F α
h : repr x = { fst := a, snd := f }
⊢ g (abs ((TypeVec.id ::: recF g) <$$> (TypeVec.id ::: fixToW) <$$> { fst := a, snd := f })) =
    g ((TypeVec.id ::: rec g) <$$> x)
rw [← MvPFunctor.comp_map, abs_map, ← h, abs_repr, ← appendFun_comp, id_comp, this]
case h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
⊢ ∀ (x : Fix F α), (recF g ∘ fixToW) x = rec g x
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
⊢ recF g ∘ fixToW = rec g
apply funext
case h.a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
⊢ ∀ (a : MvPFunctor.W (P F) α), (recF g ∘ fixToW) (Quotient.mk (wSetoid α) a) = rec g (Quotient.mk (wSetoid α) a)
case h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
⊢ ∀ (x : Fix F α), (recF g ∘ fixToW) x = rec g x
apply Quotient.ind
case h.a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x✝ : F (α ::: Fix F α)
x : MvPFunctor.W (P F) α
⊢ (recF g ∘ fixToW) (Quotient.mk (wSetoid α) x) = rec g (Quotient.mk (wSetoid α) x)
case h.a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
⊢ ∀ (a : MvPFunctor.W (P F) α), (recF g ∘ fixToW) (Quotient.mk (wSetoid α) a) = rec g (Quotient.mk (wSetoid α) a)
intro x
case h.a.a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x✝ : F (α ::: Fix F α)
x : MvPFunctor.W (P F) α
⊢ WEquiv (fixToW (Quotient.mk (wSetoid α) x)) x
case h.a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x✝ : F (α ::: Fix F α)
x : MvPFunctor.W (P F) α
⊢ (recF g ∘ fixToW) (Quotient.mk (wSetoid α) x) = rec g (Quotient.mk (wSetoid α) x)
apply recF_eq_of_wEquiv
no goals
case h.a.a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x✝ : F (α ::: Fix F α)
x : MvPFunctor.W (P F) α
⊢ WEquiv (fixToW (Quotient.mk (wSetoid α) x)) x
apply wrepr_equiv