F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x : F (Fix F)
⊢ rec (Functor.map mk) (mk x) = x
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x : F (Fix F)
⊢ dest (mk x) = x
unfold Fix.dest
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x : F (Fix F)
⊢ (mk ∘ dest) <$> x = x
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x : F (Fix F)
⊢ rec (Functor.map mk) (mk x) = x
rw [Fix.rec_eq, ← Fix.dest, ← comp_map]
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x : F (Fix F)
⊢ (mk ∘ dest) <$> x = id <$> x
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x : F (Fix F)
⊢ (mk ∘ dest) <$> x = x
conv =>
  rhs
  rw [← id_map x]
case e_a.h
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x✝ : F (Fix F)
x : Fix F
⊢ (mk ∘ dest) x = id x
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x : F (Fix F)
⊢ (mk ∘ dest) <$> x = id <$> x
congr with x
no goals
case e_a.h
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x✝ : F (Fix F)
x : Fix F
⊢ (mk ∘ dest) x = id x
apply Fix.mk_dest