## Any mpt is iso to some dc.

mpt = monotone predicate transformer. A monotone predicate transformer is a function of type (for some sets or types ) such that for all , we have . Here is the set of functions . When we are interested in equality between such functions the previous sentence actually means that is functorial.

dc = dependent container. There are two subtly different candidates for this title,
namely objects of the types

Here

The types are slightly different, and amount to different presentations of the same information. The differences may be relevant to computing with these presentations.

• In the FamFam one, we make a table where the sections are per output type, the subsections are per shape of the output sort, and the subsubsections are per position in that shape (and give an input sort).
• In the FamPow one, the subsubsections are per input type, and give the set of positions in the shape which share that input port.

There is a choice between having fixed, or on the other hand having it the carrier set in our structure, in the same way that in the theory of groups the carrier set is not globally fixed: different groups, or different dependent containers can have different carrier sets.
I have explored this only for the case I = O.

Any mpt can be expressed in (Presbyterian) disjunctive normal form , which looks like

for some (the following piece of latex compiles fine on my system).
[Unparseable or potentially dangerous latex formula. Error 2 ]
In the Pow’ variant we have a slightly different Episcopelian’ structure
(The following compiles fine on my system…)
[Unparseable or potentially dangerous latex formula. Error 2 ]

If the powerset of a set is a set, ie Pow and/or Fam : Set Set, then any monotone predicate transformer is extensionally equal to a predicate transformer in disjunctive normal form. (Extensional equality
between predicate transformers F and G means that each includes the other. That F is included in G means that for all , implies .

The proof is a piece of vacuous impredicative bollocks, where the idea is that you have an intermediate set which is actually the set of subsets of S.

I think this is interesting, because it means that impredicatively, dependent containers are a complete representation at the level of objects’. (NB, if you have impredicativity, you can define Leibnitz equality.)

There is also the level of morphisms’, where you define a notion of morphism between
predicate transformers, which may be given in disjunctive normal form. There are 3 interesting notions of
mapping between mpts and dcs, corresponding to the types
DC -> DC, DC -> MPT, and MPT -> MPT. In the case
DC -> DC, when both isotopes of DC are presbyterian (FamFam),
we have something very concrete.
Impredicatively, all these notions of mapping coincide.

With dependent containers, it seems that the statement of the representation theorem in your paper(s?)
(that there is a full and faithful functor from DC -> MPT essentially, ie. something which is at the level of morphisms,), can be strengthened to say there is actually there is even a functor which is surjective on objects.

The moral I take to be be that if you want concrete representations for mpts, you are looking for some variant
among slightly different notions of dc’s.