n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F (α ::: Fix F α)
⊢ rec (MvFunctor.map (TypeVec.id ::: mk)) (mk x) = x
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F (α ::: Fix F α)
⊢ dest (mk x) = x
unfold Fix.dest
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F (α ::: Fix F α)
⊢ ((TypeVec.id ::: mk) ⊚ (TypeVec.id ::: dest)) <$$> x = x
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F (α ::: Fix F α)
⊢ rec (MvFunctor.map (TypeVec.id ::: mk)) (mk x) = x
rw [Fix.rec_eq, ← Fix.dest, ← comp_map]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F (α ::: Fix F α)
⊢ ((TypeVec.id ::: mk) ⊚ (TypeVec.id ::: dest)) <$$> x = TypeVec.id <$$> x
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F (α ::: Fix F α)
⊢ ((TypeVec.id ::: mk) ⊚ (TypeVec.id ::: dest)) <$$> x = x
conv =>
  rhs
  rw [← MvFunctor.id_map x]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F (α ::: Fix F α)
⊢ (TypeVec.id ::: mk ∘ dest) <$$> x = TypeVec.id <$$> x
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F (α ::: Fix F α)
⊢ ((TypeVec.id ::: mk) ⊚ (TypeVec.id ::: dest)) <$$> x = TypeVec.id <$$> x
rw [← appendFun_comp, id_comp]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F (α ::: Fix F α)
this : mk ∘ dest = _root_.id
⊢ (TypeVec.id ::: mk ∘ dest) <$$> x = TypeVec.id <$$> x
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F (α ::: Fix F α)
⊢ (TypeVec.id ::: mk ∘ dest) <$$> x = TypeVec.id <$$> x
have : Fix.mk ∘ Fix.dest = _root_.id := by
  ext (x: Fix F α)
  apply Fix.mk_dest
no goals
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F (α ::: Fix F α)
this : mk ∘ dest = _root_.id
⊢ (TypeVec.id ::: mk ∘ dest) <$$> x = TypeVec.id <$$> x
rw [this, appendFun_id_id]
case h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x✝ : F (α ::: Fix F α)
x : Fix F α
⊢ (mk ∘ dest) x = _root_.id x
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F (α ::: Fix F α)
⊢ mk ∘ dest = _root_.id
ext (x: Fix F α)
no goals
case h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x✝ : F (α ::: Fix F α)
x : Fix F α
⊢ (mk ∘ dest) x = _root_.id x
apply Fix.mk_dest