Exercise 4.20 (Scott 1981, PRG-19, Lecture IV)

For approximable f, g : 𝒟 → 𝒟 prove that

fix(f ∘ g) = f(fix(g ∘ f)).

In this development f ∘ g is f.comp g, whose elementwise action is f.toElementMap ∘ g.toElementMap (toElementMap_comp). The least fixed point of an endomap is fixElement (Theorem 4.1), with its fixed-point equation toElementMap_fixElement and its least-pre-fixed-point characterization fixElement_le_of_toElementMap_le.

The proof is the classical "rolling rule" / dinaturality of the fixed-point operator: f(fix(g ∘ f)) is a fixed point of f ∘ g, hence ⊒ the least one, and a symmetric argument gives the reverse inclusion. Everything stays at the level of V.Element, so the whole file is choice-free (#print axioms ⊆ {propext, Quot.sound}).

theorem Domain.Neighborhood.ApproximableMap.comp_fixElement_isFixed {α : Type u_1} {V : NeighborhoodSystem α} (f g : ApproximableMap V V) : (f.comp g).toElementMap (f.toElementMap (g.comp f).fixElement) = f.toElementMap (g.comp f).fixElement

f(fix(g ∘ f)) is a fixed point of f ∘ g: (f ∘ g)(f(fix(g∘f))) = f((g∘f)(fix(g∘f))) = f(fix(g∘f)).

theorem Domain.Neighborhood.ApproximableMap.fixElement_comp_comm {α : Type u_1} {V : NeighborhoodSystem α} (f g : ApproximableMap V V) : (f.comp g).fixElement = f.toElementMap (g.comp f).fixElement

Exercise 4.20 (Scott 1981, PRG-19). fix(f ∘ g) = f(fix(g ∘ f)).