respectively, where here Nat is the set (object) of natural numbers and Atm is some set (object) of urelemente or *atoms*.
FM techniques propose the following:
where here [Atm]X is the *FM abstraction type*, which has properties of both a product Atm*X and a function space Atm -> X. This type does not exist in ordinary set theory (category of sets Sets), but in the closely related theory of FM sets (Schan, the Schanuel topos). It turns out that Schan admits a simple axiomatisation as a category of sets with an action by permutations (bijections) of Atm and a finiteness condition, which I shall give. We can now ask what happens if we `tweak' these axioms to consider categories of sets with other kinds of actions. I consider sets with renamings (not necessarily injective functions on Atm) and a finiteness condition. I obtain a category similar to Schan, but which supports a natural interpretation of weak HOAS.