Any mpt is iso to some dc.

mpt = monotone predicate transformer. A monotone predicate transformer is a function $$Fof type $Set^I  \to Set^O$ (for some sets or types $I,O : Set$) such that for all $U \subseteq V : I \to Set $, we have F(U) \subseteq F(V) : O \to Set. Here $U \subseteq V$ is the set of functions (\Pi i : I)U(i) \to V(i). When we are interested in equality between such functions the previous sentence actually means that $F$ is functorial.

dc = dependent container. There are two subtly different candidates for this title,
namely objects of the types
\[
       \begin{array}[t]{l}
           O \to Fam(Pow(I)) \\
          O \to Fam(Fam(I))
        \end{array}
\]
Here
\begin{array}[t]{l}
            Fam(X) = (\Sigma I : Set) I \to X \\
            Pow(X) = X \to Set.
         \end{array}
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 $I,O$ 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
\[
    U \mapsto \{ o : O | (\Sigma s : S(o) )(\Pi p : P(o,s))U(o[s/p])  \}
\]
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 $\to$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 $U, V  \subseteq S$, $U \subseteq V$ implies $F(U) \subseteq G(V)$.

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.

Leave a Reply

You must be logged in to post a comment.