Various Holy Trinities

Context, Type, Term. (Peter Dybjer's categories with families.)

       Context : Set, 
       Type    : Context -> Set,
       Term    : (Pi G : Context) Type(G) -> Set, 
       ... then whatever extra structure, eg. 
       ExtType : (Pi G : Context) Ty(G) -> Context, 
       ExtDef  : (Pi G : Context, A : Ty(G)) Tm(G,A) -> Context, 
               -- we allow contexts with definitions. 
       ...

There are surely some connections with the next trinity.

Function, relation, predicate transformer. (de Moor, Gardiner, ..)

    
        Parent, third level:
           Father : A -> Fam(Fam(B))         Mother : A -> Pow(Pow(B))   

        Child, second level:
           Son    : A -> Fam(B)              Daughter : A -> Pow(B)

                                HolyGhost : A -> B

This does not go further because the parent level "lacks pullovers". A pullover is an order enriched isotope of a pullback, something between a cardigan and a pair of flared dungarees. There is a systematic connection between the levels in which the morphisms of a higher level can be modelled as a kind of `span' in the next lower level.
This is maybe a "quintinity".
[ Anton Setzer reports that according to (Jung's interpretation of) Roman Catholic doctrine, sometime around 1963 the Virgin Mary ascended into heaven or achieved godhead. The cardinality of God may now be greater than 3. Or the powerset of natural numbers, or the continuum, for all I know. ]

State-predicate, action, specification. (Lamport)

          pred : Pow(State)
          act  : Pow(State^2)
          spec : Pow(State^w)    -- w is omega = Nat

Lamport says a (closed system) specification has the general form:

                EXISTS aux .  Init /\ []( x # x' => Act)  /\ Liveness

where Liveness is a "countable disjunction" of fairness properties

            WF_x(A) = (<>[]enabled (A /\ x # x')) => []<>(A /\ x # x')
            SF_x(A) = ([]<>enabled (A /\ x # x')) => []<>(A /\ x # x')

and EXISTS aux is a kind of existential quantification over flexible variables that is insensitive to stuttering.

Echo of Julian Bradfield's question of whether modal mu-calculus alternation hierarchy collapses at the third level. (It doesn't!)

Another theological metaphor: To break a safety property is a sin of commission. To break a liveness property is a sin of omission.

Lamports page on TLA , his specification language.

Object, Type, Kind. (de Bruijn)

The reason why this does not go further is probably that rather than introduce another level, we reflect kinds down into types, and then elaborate the new structure in the level of kinds.

An interesting question is to try to characterise as precisely as possible what a "reflection principle" is.

Addition, multiplication, exponentiation.

If we take the usual arithmetic of iterative exponents as definitions of additive combinators (0,+), multiplicative combinators (1,*) and an exponential combinator (^), it is well known that these are combinatorially complete.