F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x : Fix F
⊢ (mk ∘ dest) x = id x
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x : Fix F
⊢ mk (dest x) = x
change (Fix.mk ∘ Fix.dest) x = id x
case h
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x : Fix F
⊢ ∀ (x : F (Fix F)), (mk ∘ dest) <$> x = id <$> x → (mk ∘ dest) (mk x) = id (mk x)
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x : Fix F
⊢ (mk ∘ dest) x = id x
apply Fix.ind_rec (mk ∘ dest) id
case h
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x✝ : Fix F
x : F (Fix F)
⊢ (mk ∘ dest) <$> x = id <$> x → (mk ∘ dest) (mk x) = id (mk x)
case h
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x : Fix F
⊢ ∀ (x : F (Fix F)), (mk ∘ dest) <$> x = id <$> x → (mk ∘ dest) (mk x) = id (mk x)
intro x
case h
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x✝ : Fix F
x : F (Fix F)
⊢ mk <$> rec (Functor.map mk) <$> x = x → mk (mk <$> rec (Functor.map mk) <$> x) = mk x
case h
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x✝ : Fix F
x : F (Fix F)
⊢ (mk ∘ dest) <$> x = id <$> x → (mk ∘ dest) (mk x) = id (mk x)
rw [Function.comp_apply, id_eq, Fix.dest, Fix.rec_eq, id_map, comp_map]
case h
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x✝ : Fix F
x : F (Fix F)
h : mk <$> rec (Functor.map mk) <$> x = x
⊢ mk (mk <$> rec (Functor.map mk) <$> x) = mk x
case h
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x✝ : Fix F
x : F (Fix F)
⊢ mk <$> rec (Functor.map mk) <$> x = x → mk (mk <$> rec (Functor.map mk) <$> x) = mk x
intro h
no goals
case h
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
x✝ : Fix F
x : F (Fix F)
h : mk <$> rec (Functor.map mk) <$> x = x
⊢ mk (mk <$> rec (Functor.map mk) <$> x) = mk x
rw [h]