Add "refinement" type connective

[jonsterling]

I have discovered a much more implementable version of Orton-Pitts strictification/realignment.

1. Take a phi-modal type, i.e. A : {phi} type
2. Take family of phi-connected types indexed in A, i.e. x : {phi} A |- B(x) type \ phi. This requires Add judgmental notion of "strictly phi-connected type" #182
3. Consider the dependent sum of the above, but realigned strictly over A along phi.

The above actually accounts for all realignment situations, but it is much cleaner because the only strict isomorphisms the users has to type in are canonical isos with the unit type. This reduction simplifies implementation considerably, and makes the connective much easier to use than the traditional realignment.

To me, this connective is the basis of a modernized take on type refinements. If we add this, there is an immense amount of stuff that we could experimentally be doing...

[jonsterling]

Just for fun, here's some example code that we could write if the above existed:

axiom syn : prop
axiom tp : {syn} type
axiom tm : {syn} tp -> type

def tp* : {type | syn => tp} :=
  (syn => A : tm) * { type | syn => A}

def tm* (A : tp*) : {type | syn => tm A} :=
  snd A