Introduction

The definition of new types by carving out subsets of existing types, known as typedef, is a fundamental mechanism in Higher-Order Logic (HOL), a logic that provides the foundation for several interactive theorem provers, including HOL4 [1], HOL Light [2] and Isabelle/HOL [3]. While most of the uses of typedef are hidden under the (automated) definition of (co)inductive datatypes [4,5,6,7] and therefore not directly invoked by the users, there still remains an important scenario where typedef is invoked explicitly.

Namely, say one has a type (perhaps an algebraic datatype) 𝑇 that does not capture precisely the intended concept (because it contains too many elements), but only via an invariant defined in terms of a predicate on 𝑇, or equivalently, a set 𝐼 that has type 𝑇 set. 1 Then one defines the more precise type 𝑆 as a typedef, to consist of exactly the inhabitants of 𝑇 that belong to the set 𝐼-i.e., 𝐼 is effectively turned into a type.

Let us consider two examples, which will act as our running examples throughout this paper.

Example 1. (Distinct Lists) Polymorphic lists are introduced as the following datatype, where we use ML-style notation feature by Isabelle/HOL as well as all the HOL-based provers (in particular, 𝛼 denotes a type variable): datatype 𝛼 list = Nil | Cons 𝛼 (𝛼 list)

For a list xs, we let length xs be its length and, given a natural number 𝑖 < length, we let xs!𝑖 be the (𝑖−1)'th element in xs (so the indexing starts from 0). In some developments, one may be interested in working with nonrepetitive ("distinct") lists, i.e., lists whose elements do not repeat-to this end, one defines the Envelope g.buday@sheffield.ac.uk (G. Buday); a.popescu@sheffield.ac.uk (A. Popescu) and the following axioms stating that these functions are mutually inverse bijections between the new type 𝛼 dlist and the subset {xs ∶ 𝛼 list | distinct xs} of the base type 𝛼 list. 3 In Isabelle/HOL, these axioms are actually packed into a single axiom: In a formal development that follows the above scheme, one usually distinguishes between:

• developing the "internal" mathematical theory, which usually proceeds without defining 𝑆, but instead working with 𝑇 and stating the theorems relativized to 𝐼-for example, proving facts of the form ∀𝑡 ∶ 𝑇 . 𝑡 ∈ 𝐼 ⟶ . . . • at the end, defining 𝑆 and "sealing" the library for export by transferring from 𝑇 to 𝑆 all the constants and all the main (exportable) facts that have been proved proved relative to 𝐼-for example, turning facts of the form ∀𝑡 ∶ 𝑇 . 𝑡 ∈ 𝐼 ⟶ . . . into facts of the form ∀𝑡 ′ ∶ 𝑆. . . .

The process of "isomorphically" transferring 𝐼-relativized constants and results on 𝑇 to corresponding constants and results on 𝑆, while seemingly conceptually straightforward, turns out to be quite subtle in the presence of higher-order constants. It requires infrastructure for lifting relations along type constructors (known as relators), which allows the automated proofs of the transferred theorems from the original ones-this is facilitated in Isabelle/HOL by various dedicated tools [8,9,10].

In this short work-in-progress paper, we study a fairly common pattern: the isomorphic transfer in the presence of nested type constructors. We start with motivation in terms of a standard construction applied to our running examples ( §2), which leads to formulating the wider scope of the problem. We then work out the solution to the problem in an ad hoc manner on the running examples §3. After that, we are ready to describe our main result: some abstract general structure and conditions that enable this pattern, in that they allow constructing a back-and-forth bijection for transfer ( §4), and show how it instantiates to our examples. We conclude with related work and future plans, notably the planned integration of our work into Isabelle's Lifting and Transfer package ( §5). Our concepts and results apply to Higher-Order Logic, hence are in principle relevant to any HOL-based provers. We have formalized them in the Isabelle/HOL theorem prover, and the formal scripts are publicly available [11].

The Concrete Problem

Consider the problem of proving that the type constructors (polymorphic types) 𝛼 dlist and 𝛼 distrib constitute monads [12,13] or at least monad-like structures-which are very useful properties to have for any (data)type, whenever possible.

According to the above pattern, one wishes to first prove the properties for the underlying (representing types) 𝛼 list and 𝛼 → real relative to the defining predicates distinct and dist, and then transfer them to the defined types 𝛼 dlist and 𝛼 distrib. (Not only is this good practice, but in some sense it is the only way to proceed, at least initially when "bootstrapping" a theory for the defined types, given that initially our only means to prove a property on the defined type is to trace it back to a property on the underlying type.) Some of the monadic structure and properties involve nesting the application of type constructors, for example we want to have a map (functorial-action) operator map distrib ∶ (𝛼 → 𝛽) → (𝛼 distrib → 𝛽 distrib) and join (counit) operator join distrib ∶ (𝛼 distrib) distrib → 𝛼 distrib satisfying (among others) the associativity law join distrib ∘ (map distrib join distrib ) = join distrib ∘ join distrib .

How to define such structure and prove such properties on the defined types? Let us start with a simple example that does not involve nesting, namely defining the map operator on (𝛼 → 𝛽) → (𝛼 distrib → 𝛽 distrib) and proving that it preserves identities, in that ∀𝑑 ∶ 𝛼 distrib. map distrib (id ∶ 𝛼 → 𝛼) 𝑑 = 𝑑 where id denotes the identity function. We define map distrib on any 𝑔 ∶ 𝛼 → 𝛽 and 𝑑 ∶ 𝛼 distrib by map distrib 𝑔 𝑑 = Abs distrib (𝜆𝑏 ∶ 𝛽. ∑ 𝑎∈𝑔 −1 𝑏 Rep distrib 𝑑 𝑎). Notice that the definition requires a backand-forth application of the abstraction and representation functions Abs distrib and Rep distrib , with some specific manipulation of items of the underlying type 𝛼 → real. (In this case, the specific manipulation happens to involve taking the sum of a function in 𝛼 → real over all the elements of the 𝑔-preimage of 𝑔, but the exact nature of such manipulations is not important here.) Now, to prove the desired fact, fix 𝑑 ∶ 𝛼 distrib. In order to show map distrib id 𝑑 = 𝑑, by the injectivity of Rep distrib it suffixes to show Rep distrib (map distrib id 𝑑) = Rep distrib 𝑑. Using the definition of map distrib and the fact that Rep distrib is left-inverse to Abs distrib , the above is equivalent to 𝜆𝑏 ∶ 𝛽. ∑ 𝑎∈id −1 𝑏 Rep distrib 𝑑 𝑎 = Rep distrib 𝑑, i.e., to 𝜆𝑏 ∶ 𝛽. ∑ 𝑎=𝑏 Rep distrib 𝑑 𝑎 = Rep distrib 𝑑, which follows from the properties of sums and function extensionality.

We thus have the following pattern: To define constants on the defined type and prove properties for them, we need to move back and forth via the abstraction-representation pair and use consequences of the associated type_definition axiom.

But how to do this in the presence of nested defined type constructors (where the abstractionrepresentation pairs stemming from type definitions no longer work out of the box)? In the next section, we discuss in an ad hoc manner how to tackle the nested isomorphic transfer problem in the presence of nested types for our two running examples. After that, we will introduce an abstract solution, which covers these two cases and many others.

The Solution for Two Concrete Instances

Now let us come back to the original more complex problem, of defining join distrib ∶ (𝛼 distrib) distrib → 𝛼 distrib (in addition to map distrib which we have already defined) and proving the associativity law.

In order to define join distrib , which operates on the nested defined type (𝛼 distrib) distrib, we need an understanding of how a counterpart of this operator should act on the (nested application of) the underlying type, i.e., on (𝛼 → real)real. To be more exact, we don't need to consider the behavior of such a counterpart on all functions 𝐹 ∶ (𝛼 → real) → real, but seemingly only on functions that act like distributions, i.e., satisfy distrib 𝐹 (i.e., are positive, have countable support and sum to 1). In fact, upon a closer look we see that the functions of interest are not really distributions on the entire type 𝛼 → real, but on the subset of 𝛼 → real that consists of distributions only, i.e., distributions on the set {𝑓 ∶ 𝛼 → real | distrib 𝑓 }. In other words, we need a relativized version of the predicate distrib, let us denote it by distOn ∶ 𝛼 set → 𝛼 distrib → bool, defined by

distOn 𝐴 𝑓 ≡ (∀𝑥 ∶ 𝛼. 𝑥 ∈ 𝐴 ⟶𝑓 𝑥 ≥ 0) ∧ countable {𝑥 ∶ 𝛼 | 𝑥 ∈ 𝐴 ∧𝑓 𝑥 ≠ 0} ∧ ∑ 𝑥∈𝐴 𝑓 𝑥 = 1

where we have highlighted the difference from the original predicate dist-in that the conditions are not applied to the entire type 𝛼, but to a parameter subset 𝐴 ∶ 𝛼 set. Note that we can recover the original predicate as dist = distOn UNIV, where UNIV is the "universal" set covering the entire type.

With this relativized predicate at hand, the picture becomes clear: Given a function 𝐹 ∶ (𝛼 → real) → real that acts like a distribution on distributions on 𝛼, i.e., such that distOn {𝑓 ∶ 𝛼 → real | dist 𝑓 } 𝐹 holds, we have the formal means to turn it into a "flat" distribution, let us call it join 𝐹, on 𝛼 → real, namely by summation (applying of course a well-known mathematical construction): join 𝐹 𝑥 ≡ ∑ 𝑓 ∈{𝑓 | dist 𝑓 } 𝐹 𝑓 𝑥. Now, to define join distrib from join, we need to able to move back and forth between 𝛼 distrib distrib and and (𝛼 → real) → real, ideally using a similar infrastructure as the abstraction-representation pair (Abs distrib , Rep distrib ) and predicate distrib that allowed us to move between 𝛼 distrib and 𝛼 → real. And indeed, this is possible:

• We define dist 2 ∶ ((𝛼 → real) → real) → bool to be distOn {𝑓 ∶ 𝛼 → real | dist 𝑓 }. • We define Abs distrib,2 ∶ ((𝛼 → real) → real) → (𝛼 distrib) distrib by Abs distrib,2 𝐹 = Abs distrib (𝜆 𝑑 ∶ 𝛼 distrib. 𝐹 (Rep distrib 𝑑)). • We define Rep distrib,2 ∶ (𝛼 distrib) distrib → ((𝛼 → real) → real) by Rep distrib,2 𝐷 = 𝜆𝑓 ∶ 𝛼 → real. Rep distrib 𝐷 (Abs distrib 𝑓 ).

Note that we defined distrib 2 in line with the above analysis, and defined Abs distrib,2 and Rep distrib,2 with the aim of achieving a bijective correspondence between (𝛼 distrib) distrib and the elements of With the goal of a general solution in mind, let us note some similarities and commonalities of the above two cases. While for distinct lists the definitions of the one-level-up abstraction and representation functions involve entities of the same kind (namely abstractions for abstractions and representations for representations), in the case of distributions the definitions combine the two, for example the definition of the one-level-up abstraction uses outer abstraction together with inner representation. This is a reflection of lists being a covariant functor and function-space-to-reals being a contravariant functor.

(𝛼 → real) → real satisfyig dist 2 .

The common pattern of the two is, however, the fact that the one-level-up operators employ composition between an (1) operator and (2) the map function for the given functor applied to an operator. This is manifestly clear for distinct lists, for example the one-level-up abstraction Abs dlist,2 is the composition of Abs dlist with map list Rep dlist ; for distributions, this is also seen to be the case, if we note that the map function for the contravariant functor 𝛼 → real is 𝜆𝑔 ∶ 𝛼 → 𝛽. 𝜆𝑓 ∶ 𝛽 → real. 𝑔 ∘ 𝑓.

Another discrepancy between the two cases is the definition of the one-level-up characteristic predicates (distrib 2 versus distinct 2 ); as we will see next, we will be able to uniformly capture both cases under a more general set-lifting operator.

An Abstract Formulation of the Problem and a General Solution

We formulate the problem abstractly as follows: How to lift the abstraction-representation properties characteristic of type definitions to nested applications of the defined type constructor? In the previous section, we have discussed solutions to two instances of this problem. The first instance is representayive of a wide class of situations, namely polymorphic inductive datatypes (which are all covariant functors) with invariants; the second also has some cousins in the formalization and specification literature, for example the defined types topological filters and of mutisets, as well as variations such as discrete subdistributions. In what follows, we introduce a generalization that covers all these cases.

In

Assumptions. We assume that the underlying type constructor 𝛼 𝑇 comes equipped with an operator Trel ∶ 𝛼 set → 𝛽 set → (𝛼 → 𝛽 → bool) → (𝛼 𝑇 → 𝛽 𝑇 → bool) for lifting relations to 𝑇 that for bijective relations commutes with composition; namely, letting bijBetw 𝐴 𝐵 𝑅 express that the relation 𝑅 is a bijection between 𝐴 and 𝐵:

(A1) bijBetw 𝐴 𝐵 𝑃 and bijBetw 𝐵 𝐶 𝑄 implies Trel 𝐴 𝐶 (𝑃 ∘ 𝑄) = Trel 𝐴 𝐵 𝑃 ∘ Trel 𝐵 𝐶 𝑄 for all 𝐴, 𝐵, 𝐶, 𝑃, 𝑄 Moreover, we assume that there exists an operator Iset ∶ 𝛼 set → (𝛼 𝑇 ) set for lifting sets to 𝑇, which is an extension of 𝐼 in that (A2) Iset UNIV = 𝐼 and the following hold, where eqOn 𝐴 𝑅 says that the restriction of 𝑅 to 𝐴 is the equality on (i.e., the diagonal of) 𝐴:

(A3) bijBetw 𝐴 𝐵 𝑅 implies bijBetw (Iset 𝐴) (Iset 𝐵) (Trel 𝐴 𝐵 𝑅) for all 𝐴, 𝐵, 𝑅 (A4) bijBetw 𝐴 𝐴 𝑅 and eqOn 𝐴 𝑅 implies eqOn (Iset 𝐴) (Trel 𝐴 𝐴 𝑅) for all 𝐴, 𝑅 𝑇 together with the operator Trel forms a relator-like structure [14,15], similar to those that underlie Isabelle/HOL's transfer tool [8] and datatype specification mechanism [6]. However, this concept comes with an explicit indication of the domain and codomain sets and targets bijections between these sets. In particular, (A1) only requires Trel to commute with (relation) composition when restricted to bijective relations. While we think of Trel as being associated to 𝑇, we think of Iset as being associated to the invariant 𝐼 (which it generalizes via (A2)). For example, if 𝑇 is list, then it is reasonable to take Trel to be the list relator (relating lists position-wise), but we have no reason to commit to Iset as being the standard set operator associated to lists (returning the set of all elements of a list)-rather, the choice of Iset will depend on what invariant we want to consider on lists. Of course, as the axiom (A2) suggests, the Iset parameter of our abstract framework is reminiscent of the relativized version of the predicate dist that we employed in the case of distributions.

Trel and Iset are connected by the assumptions (A3) and (A4). Thus, (A3) states that Trel lifts bijections between two sets to bijections between the Iset-liftings of these sets, which roughly means that Iset partially acts like a subrelator of (𝑇 , Trel). Finally, (A4) is an Iset-relativization of the standard property of relators of preserving equalities-namely, here we say Trel preserves partial equalities w.r.t. Iset.

Let us see how to instantiate this framework to our running examples. To this end, we first note that having chosen our assumptions in terms of relations rather than functions allows us to capture both covariant and contravariant cases. For the case of the distribution type 𝛼 distrib, we take:

• 𝛼 𝑇 to be 𝛼 → real;

• Trel 𝐴 𝐵 𝑅 𝑓 𝑔 to be ⇒ real (𝜆𝑎, 𝑏. 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑅 𝑎 𝑏) 𝑓 𝑔 ∧ (∀𝑎 ∉ 𝐴. 𝑓 𝑎 = ⊥) ∧ (∀𝑏 ∉ 𝐵. 𝑔 𝑏 = ⊥), where ⊥ is a (polymorphic) fixed "undefined" element (which is available in HOL on each type via Hilbert choice) and ⇒ real is the real-instance of the function-space relator, defined by ⇒ real 𝑃 𝑓 𝑔 ≡ ∀𝑎, 𝑏. 𝑃 𝑎 𝑏 ⟶ 𝑓 𝑎 = 𝑔 𝑏; • Iset to be given by the relativized form of the distOn predicate, namely Iset 𝐴 ≡ {𝑓 | distOn 𝐴 𝑓 }.

For the case of the distinct-list type 𝛼 dlist, we take:

• 𝛼 𝑇 to be 𝛼 list;

• Trel 𝐴 𝐵 to be the list relator list_all, where list_all 𝑅 relates two lists just in case they have the same length and their elements are position-wise related (thus, the domain and codomain sets are ignored by Trel); • Iset to be defined as Iset 𝐴 ≡ {xs | distinct xs ∧ set xs ⊆ 𝐴}, where set ∶ 𝛼 list → 𝛼 set is the support operator for lists (returning the set of all elements of a list).

Note the two flavors of instantiating the relativized operator Iset, depending on whether we deal with a contravariant or covariant functor, namely : (1) either, in the contravariant case, by relativizing the original predicate dist to distOn; (2) or, in the covariant case, by intersecting the original predicate distinct with the adjoint of the support operator (which is usually available for covariant functors, and in particular is available for all container types)-indeed, the righthand side of the definition of Iset 𝐴 can be written as {xs | distinct xs} ∩ {𝑥𝑠 | set xs ⊆ 𝐴}, and the operator 𝐿 = 𝜆𝐴. {𝑥𝑠 | set xs ⊆ 𝐴} is the right adjoint4 of the support operator set in the sense that xs ∈ 𝐿 𝐴 iff set xs ⊆ 𝐴. It is relatively easy to check that these instances satisfy our assumptions. For example, (A3) in the case of the distribution instantiation says that a bijection between two sets 𝐴 and 𝐵 induces a bijection the sets of distributions on 𝐴 and 𝐵 respectively, which are constant ⊥ outside 𝐴 and 𝐵 respectively.

Our main result is that these abstract assumptions are sufficient for solving our problem, thus generalizing the constructions in the above particular cases (and in many other cases, e.g., any datatypes with invariants turned into typedefs).

Theorem: Under the assumptions (A1)-(A4) above, we have a solution to our problem for all 𝑛 ≥ 1, in that there exist 𝐼 𝑛 ∶ (𝛼 𝑇 𝑛 ) set, Abs 𝑆,𝑛 ∶ 𝛼 𝑇 𝑛 → 𝛼 𝑆 𝑛 and Rep 𝑇 ,𝑛 ∶ 𝛼 𝑇 𝑛 → 𝛼 𝑆 𝑛 such that type_definition Abs 𝑆,𝑛 Rep 𝑇 ,𝑛 𝐼 𝑛 holds.

A formal proof in Isabelle/HOL of the core of this theorem can be found in [11]; due to the HOL type system limitations, the formal proof is restricted to the case when 𝑛 = 2, but also indicates how to iterate the argument for arbitrary 𝑛 and shows the iterations for 3 and 4.

Proof sketch. We proceed by induction on 𝑛. For 𝑛 = 1, we simply take 𝐼 𝑛 = 𝐼, Abs 𝑆,𝑛 = Abs 𝑆 and Rep 𝑆,𝑛 = Rep 𝑆 , so the desired fact holds by our assumptions.

For the induction step, assume that we have 𝐼 𝑛 ∶ (𝛼 𝑇 𝑛 ) set, Abs 𝑆,𝑛 ∶ 𝛼 𝑇 𝑛 → 𝛼 𝑆 𝑛 and Rep 𝑇 ,𝑛 ∶ 𝛼 𝑇 𝑛 → 𝛼 𝑆 𝑛 such that type_definition Abs 𝑆,𝑛 Rep 𝑇 ,𝑛 𝐼 𝑛 holds. We define 𝐼 𝑛+1 ∶ (𝛼 𝑇 𝑛+1 ) set, Abs 𝑆,𝑛+1 ∶ 𝛼 𝑇 𝑛+1 → 𝛼 𝑆 𝑛+1 and Rep 𝑇 ,𝑛+1 ∶ 𝛼 𝑇 𝑛+1 → 𝛼 𝑆 𝑛+1 as follows:

𝐼 𝑛+1 ≡ Iset 𝐼 𝑛 ; Abs 𝑆,𝑛+1 = Abs 𝑆 ∘ funOf (Trel (relOf Abs 𝑆,𝑛 )); Rep 𝑆,𝑛+1 = Rep 𝑆 ∘ funOf (Trel (relOf Rep 𝑆,𝑛 )).

Above, the operators relOf ∶ (𝛼 → 𝛽) → (𝛼 → 𝛽 → bool) and funOf ∶ (𝛼 → 𝛽 → bool) → (𝛼 → 𝛽) provide back and forth conversions between bijective relations and (partially) bijective functins. Namely, we have the following properties for them, where bij_betw 𝐴 𝐵 𝑓 says that the restriction of the function 𝑓 ∶ 𝛼 → 𝛽 to 𝐴 ∶ 𝛼 set is a bijection between 𝐴 and 𝐵 ∶ 𝛽 set: (1) If bij_betw 𝐴 𝐵 𝑓, then bijBetw 𝐴 𝐵 (relOf 𝑓 ) and funOf (relOf 𝑓 ) = 𝑓; (2) If bijBetw 𝐴 𝐵 𝑅, then bij_betw 𝐴 𝐵 (funOf 𝑅) and relOf (funOf 𝑓 𝑅 = 𝑅.

To prove type_definition Abs 𝑆,𝑛+1 Rep 𝑇 ,𝑛+1 𝐼 𝑛+1 compositionally (along the definitions of the abstraction ad represenations operators), we introduce a generalization of type_definition that does not assume one of its argument functions (namely the representation function) to operate on the entire domain, but on an additional parameter set. Namely, we define bij_pair ∶ (𝛽 → 𝛼) → (𝛼 → 𝛽) → 𝛽 set → 𝛼 set → bool as follows, where we highlight the differences from type_definition: bij_pair 𝑟 𝑎 𝐵𝐴 ≡ (∀𝑦. 𝑦 ∈ 𝐵 ⟶ 𝑟 𝑦 ∈ 𝐴) ∧ (∀𝑥. 𝑥 ∈ 𝐴 ⟶ 𝑎 𝑥 ∈ 𝐵) ∧ (∀𝑦 ∶ 𝛽. 𝑦 ∈ 𝐵 ⟶ 𝑎 (𝑟 𝑦) = 𝑦) ∧ (∀𝑥 ∶ 𝛼. 𝑥 ∈ 𝐴 ⟶ 𝑟 (𝑎 𝑥) = 𝑥). Thus, bij_pair 𝑟 𝑎 𝐵 𝐴 says that 𝑎 and 𝑟 are mutually inverse bijections between 𝐴 and 𝐵; in particular, we have (3) bij_pair 𝑟 𝑎 𝐵 𝐴 = type_definition 𝑟 𝑎 UNIV 𝐴.

Next, we define the relational counterpart of bij_pair, namely bijPair ∶ (𝛽 → 𝛼 → bool) → (𝛼 → 𝛽 → bool) → 𝛽 set → 𝛼 set → bool, such that bijPair 𝑃 𝑄 𝐵 𝐴 says that 𝑃 and 𝑄 are mutually inverse (relational) bijections between 𝐴 and 𝐵. The operators bij_pair and bijPair correspond to each other via the translations between functions and relations: (4) If bij_pair 𝑟 𝑎 𝐵 𝐴 then bijPair (relOf 𝑟) (relOf 𝑎) 𝐵 𝐴;

(5) If bijPair 𝑃 𝑄 𝐵 𝐴 then bij_pair (funOf 𝑃) (funOf 𝑄) 𝐵 𝐴. They also commute with relation and function composition: (6) If bij_pair 𝑟 𝑎 𝐵 𝐴 and bij_pair 𝑟 ′ 𝑎 ′ 𝐴 𝐶 then bij_pair (𝑟 ′ ∘ 𝑟) (𝑎 ′ ∘ 𝑎) 𝐵 𝐶; (7) If bijPair 𝑃 𝑄 𝐵 𝐴 and bij_pair 𝑃 ′ 𝑄 ′ 𝐴 𝐶 then bijPair (𝑃 ∘ 𝑃 ′ ) (𝑄 ∘ 𝑄 ′ ) 𝐵 𝐶.

Finally, using (A1), (A3) and (A4), we can prove the crucial property that Trel "lifts" the bijPair property relative to Iset: (8) If bijPair 𝑃 𝑄 𝐴 𝐵 then bijPair (Trel 𝐴 𝐵 𝑃) (Trel 𝐵 𝐴 𝑄) (Iset 𝐴) (Iset 𝐵). □

Note that the theorem asserts the existence of 𝑛-level predicates 𝐼 𝑛 and abstraction-representation pairs (Abs 𝑛 , Rep 𝑛 ) which extend the original ones, 𝐼 and (Abs, Rep). But the question arises on whether these are the "right" extensions. The answer relies only on the suitability of 𝐼 𝑛 , since once that is decided than any projection pair (Abs 𝑛 , Rep 𝑛 ) satisfying type_definition Abs 𝑆,𝑛 Rep 𝑇 ,𝑛 𝐼 𝑛 would do-mirroring the fact that in a type definition (at level 1) only 𝐼 matters and any (Abs, Rep) satisfying type_definition Abs 𝑆 Rep 𝑇 𝐼 is as good as any other. Now, concerning the suitability of 𝐼 𝑛 , we note from the proof that 𝐼 𝑛 = Iset 𝑛 UNIV; so it all hinges upon whether Iset is the "right" way of lifting sets of elements of 𝛼 to sets of elements of 𝛼 𝑇 that respects the intended meaning of the subset 𝐼 of 𝛼 𝑇. In other words, whatever concept 𝐼 is supposed to represent, we want that Iset provides a correct relativization of that concept from the entire type 𝛼 to a subset 𝐴 ∶ 𝛼 𝑠𝑒𝑡. Our assumptions (A2)-(A4) are sanity properties for such a relativization, but whether this is the correct relativization needs to be established in each particular case-in other words, it is the responsability of the user of our framework to provide a correct and meaningful Iset operator. This is easily seen to be the case in our two examples, where the move from 𝐼 to Iset clearly represents the move from distributions on the whole type to distributions on a given subset, and from distinct lists on the whole type to distinct lists on a given subset, respectively. Moreover, the scheme that worked for distinct lists (of intersecting with the support operator) works for essentially the same reason for any container type.

Finally, a remark on the generality of the theorem: While we have formulated it in reference to the (possibly iterated) nesting of a single type constructor, the construction and proof can be straightforwardly (albeit tediously) extended to cope with combining / nesting different type constructors (which can also have more than one argument).

Related Work and Future Work

Isomorphic transfer is an important topic in formal reasoning, and is one of the main motivations of major recent developments such as Homotopy Type Theory [16]. Transfer along ismorphisms, as well as along quotient projections and refinements, is also well represented in the world of HOL-based provers (and especially Isabelle/HOL), e.g., [17,18,19,8,20,21]. In dependent type theory, problems similar to the ones we address here are formulated in the context of (partial) setoids [22,23], and proof assistants such as Coq [24] (via SSReflect [25]) and Lean [26] offer quasi-automated mechanisms to address them, thus mitigating what is referred to as "setoid hell", i.e., the need to prove over and over again that certain (partial) equivalence relations are preserved by the defined functions. Note that the problem we addressed in this paper, which has to do with relativization to sets, is a particular case of relativization to partial equivalence relations-and in fact dealing with the former at higher-order types quickly escalates to having to deal with the latter, even in the absence of dependent types [10].

Another technical part of our setting concerns the HOL defined types, which are not included in their base types but only injected into them. Other formalisms offer pure subtyping / inclusion mechanisms, notably PVS [27], F ⋆ [28], and logical frameworks featuring refinement types [29]-where the goal of isomorphic transfer is replaced by corresponding goals concerning automating aspects of type checking.

Next, we will focus on the most closely related work, namely Isabelle's Lifting and Transfer package [30,8]. From the very beginning, the authors of this tool have been aware of the potential difficulties raised by nested type constructors, and have implemented a solution based on parameterized transfer relations. For example, in the case of distrib, the current implementation defines automatically a relation in (𝛼 → real) → 𝛽 distrib → bool (thus using different type variables 𝛼 and 𝛽) as the composition between the relator ⇒ real and the relational version of Abs distrib . This does not guarantee an isomorphic relationship between nested applications of (_ → real) and distrib like our framework does (exported as a type_definition theorem), but offers enough infrastructure in order to allow the user to "lift" the definition of constants from (_ → real) to distrib even in the presence of nesting. Since the relativized defining set is not provided explicitly (like in our framework, as the operator Iset), the proof goals arising when transferring theorems containing such constants are quite intricate and convoluted, in sharp contrast to the non-nested case. On the other hand, at the expense of asking the user to provide more information (not just the relator Trel but also the operator Iset) and proving some sanity properties, our approach really flattens everything to the "first-order" non-nesting case-with the potential of simplifying the proof goals. Moreover, currently the transfer package relies on a parametricity theorem for the defined type's underlying predicate, which our approach does not. Overall, our approach requires some more initial effort from the user upon introducing a new type, but this has the potential to pay off in the later stages of the developments.

This having been said, our work addresses only a subproblem of the overall lifting and transfer problem, which the Lifting and Transfer package addresses quite comprehensively. So we do not envision our development as an alternative to this mature tool, but as a possible "add-on" that can improve the usability and automation of the tool's handling of nested types. Since what we produce for nested types are type_definition theorems, these can in principle be directly integrated into the Lifting and Transfer package (via the "setup_lifting" command), save for one difficulty caused by the fact that any provided abstraction operators are currently required to be registered as dataype-like constructors-addressing this formal engineering problem is ongoing work. (Of course, the integration will involve the fully general case, of different type constructors of possible multiple arguments nested in arbitrary ways.)

Another short-term plan is to provide some generic infrastructure that automates our inferred result for arbitrary type constructors, which can then be instantiated to different cases. This is being tackled (in joint work with Dmitriy Traytel) with the help of a quasi-foundational developement of polymorphic locales, generalizing Isabelle's standard (monomorphic) locales [31,32] in a manner that does not impair the meta-properties of the logic and definitional mechanisms underlying Isabelle/HOL [33,34,35,36].