+### Equality
+
+What we have to decide here is which models we admit. The paper does not
+mention quotiented sets, thus using an intensional equality is enough
+to capture the intended content of the paper. Nevertheless, the formalization
+cannot be reused in a concrete example where the (families of) sets
+that will build the axiom set are quotiented.
+
+Matita gives support for setoid rewriting under a context built with
+non dependent morphisms. As we will detail later, if we assume a generic
+equality over the carrier of our axiom set, a non trivial inductive
+construction over the ordinals has to be proved to respect extensionality
+(i.e. if the input is an extensional set, also the output is).
+The proof requires to rewrite under the context formed by the family of sets
+`I` and `D`, that have a dependent type. Declaring them as dependently typed
+morphisms is possible, but Matita does not provide an adequate support for them,
+and would thus need more effort than formalizing the whole paper.
+
+Anyway, in a preliminary attempt of formalization, we tried the setoid approach,
+reaching the end of the formalization, but we had to assume the proof
+of the extensionality of the `U_x` construction (while there is no
+need to assume the same property for `F_x`!).
+
+The current version of the formalization uses `Id`.
+