Mobile

Given a type A we define a quotient inductive type $\mathrm{Mobile}A$ with the following constructors:

• $\mathrm{leaf}:\mathrm{Mobile}A$
• $\mathrm{node}:(A\to \mathrm{Mobile}A)\to \mathrm{Mobile}A$
• $\mathrm{perm}:\forall f(\pi :A\leftrightarrow A)\to \mathrm{node}f=\mathrm{node}(f\circ \pi )$

References

altenkirch2016-qiit