The framework used for this novel presentation is the so called bi-directional typesetting. It seems possible to define the impredicative quantification and intersection types as necessary for impredicative representation of inductive and coinductive types supporting dependent elimination (as in http://firsov.ee/impred-ind/impred-ind.pdf, “Generic Derivation of Induction for Impredicative Encodings in Cedille” by Denis Firsov and Aaron Stump).

Let's settle the notation and tell a little bit more about the bi-directional approach. In this approach two kinds of terms: typed terms and untyped terms. Typed terms know their type, untyped can be typechecked against a type. We will have two kinds of typing jugdements:

1) `t : T` — the (typed term) `t` has the canonical type `T` which can be read out of the term `t`

2) `T ∍ t` — the type `T` admits the term `t` as an inhabitant. In other words, `t` typechecks when used where a value of the type `T` is required. Here `t` can be both untyped or typed: we are allowed to forget about canonical types and typecheck terms otherwise. It will be quite handy when one is to replace the single universe `∗` belonging to itself (the source of the inconsistency) by a series of cummulative universes belonging to each other: `U : U' : U'' :...`. There each term belonging to a universe `U` also typechecks as a value of `U'` and by extension also of `U''` and so on. The ability to insert a typed term everywhere an untyped is required neglecting the canonical type can be formulated either as a computation rule, or as a property of the framework. I prefer the latter.

Once an expression `t` is typechecked with respect to `T`, it can be coerced to have `T` as its canonical type. We'll use the notation `t : T` for coersion/raw term annotation. (I'm sorry to use my own notation inconsistent with Conor's, yet consistent with some extensions we're working on.) This gives us the first rule:

```

∗ ∍ T T ∍ t ———————————————— (t : T) : T```

(Given an expression `T` admissible as a type and expression `t` admissible as a `T`, the expression `(t : T)` is a typed expression with canonical type `T`.)

The rest of the typing rules (we omit some bureaucratic clutter) read as follows:

```

——————— ∗ ∍ ∗```

The expresson `∗` is admissible as a type.

```

x : S ⊢ ∗ ∍ T(x) —————————————————— ∗ ∍ (\x : S) ⟶ T```

Given an expression `T` admissible as a type, written in a context extended with additional symbol `x` typed as `S`, we can write down the expression `(\x : S) ⟶ T`, which is admissible as type.

```

x : S ⊢ T(x) ∍ t(x) ——————————————————————————— ((\x : S) ⟶ T) ∍ (\x ↦ t)```

Given a term `t` admissible as a `T`, both written in a context extended with additional symbol `x` typed as `S`, we can write down the expression `\x ↦ t`, which is admissible as a dependent function `(\x : S) ⟶ T`.

The only thing we have to write down yet is the function application and the computation rule for it:

```

f : (\x : S) ⟶ T(x) S ∍ s ——————————————————————————————— (f s) : T(s : S) (\x ↦ t(x) : (\x : S) ⟶ T(x)) s ⇝ t(s : S) : T(s : S)```

I'm very interested about making this system stratified. But once we do so, we won't be able to encode interesting types via their impredicative encoding. So let's define a parametric quantifier as a remedy. It's very much like a function type, but the variable the output type is dependent on cannot be used in the underlying term computationally.

The type former rule would be exactly like the one for the dependent function:

```

x : P ⊢ ∗ ∍ T(x) —————————————————— ∗ ∍ ∀(\x : P), T```

Yet we won't have any constructor for this type. We'll only note that an untyped expression of the valid form is admissible for this type:

```

x : P ⊢ T(x) ∍ t ———————————————————— (∀(\x : P), T) ∍ t```

Yet we will introduce a sort of application (instantiation at a concrete value) and a computation rule for it:

```

f : ∀(\x : P), T(x) P ∍ p —————————————————————————————— f[p] : T(p : P) (t : ∀(\x : P), T(x))[p] ⇝ t : T(p : P)```

(Maybe in future we should insist on the premise `p : P` instead of `P ∍ p` while forbidding usage of `∗` on right of the coercive annotation operator ` : ` while allowing to use universes of finite level instead. The best thing is to allow `ideal types` like `∗` or `∗ ⟶ ∗` in the left part of the typechecking judgement ` ∍ ` and for parametric quantification, while insisting on instantiation with concrete types, including universes of a finite level. Together with propositional resizing rules, one would possibly obtain a sufficient form of large elimination without encountering the Hurkens' paradox.)

The great hope is that this way (once the universes are stratified) we would be able to reconstruct the Calculus of Construction with parametric quantifier.

To give you an idea, how impredicative encodings of coinductive and inductive types work, I'll give two examples. First off, the dependent pair:

```

∀(\C : ∗), (\observer : ∀(\X : ∗), (\x : X) ⟶ (\fst : X ⟶ A) ⟶ (\snd : X ⟶ B(fst x)) ⟶ C) ⟶ C```

A pair-`observer` a thing that gets a value `x` of an unknown type `X` together with

- a function `fst : X ⟶ A` extracting a value of the type `A` from `x` and

- a function `snd : X ⟶ B(fst x)` extracting a value of the type `B(fst x)` from `x`,

and returns a C. Pair is precisely the object behaviorily defined by its ability to parametrically compute a value of type `C` from any `C`-valued pair-`observer`.

Now, natural numbers can be defined by their ability to apply a function `step : X ⟶ X` for any type `X` any fixed number of times:

```

∀(\X : ∗), (\step : X ⟶ X) ⟶ (\base : X) ⟶ X```

However, in CC with parametric quantifiers we're still unable to provide dependent elimination for inductive types. i.e. induction which is a fundamental for carrying out any proofs. Recent result of Firsov and Stump shows that it is possible to derive induction (the issue of large elimination being suppresed for a start) using the so called dependent intersection types. It seems they are definable within the bi-directional framework too! (Well, actually I'm not sure, there are lot of details which could possibly go wrong, but still it is interesting to try.)

The familiar type former rule:

```

x : T ⊢ ∗ ∍ R(x) ———————————————————— ∗ ∍ (\x : T) ∩ R(x)```

Now the interesting stuff:

```

x : T ⊢ R(x) ∍ x ———————————————————— (\x : T) ∩ R(x) ∍ x```

If a term `x` is admissible for a type `R(x)` (dependent on `x`, whoa), than it is also admissible for the type `(\x : T) ∩ R(x)`.

The main raison d'être for this construction is so far the following usage:

Let

```

CNat := ∀(\X : ∗), (\step : X ⟶ X) ⟶ (\base : X) ⟶ X ze := \step ↦ \base ↦ base su := \n ↦ \step ↦ \base ↦ step (n base) Nat := (\n : CNat) ∩ ∀(\P : CNat ⟶ ∗), (\step : ∀(\m : CNat), P(m) ⟶ P(su m)) ⟶ (\base : P(ze)) ⟶ P(n) elim-Nat = (\step ↦ \base ↦ \n ↦ n step base) : ∀(\P : Nat ⟶ ∗), (\step : ∀(\m : Nat), P(m) ⟶ P(su m)) ⟶ (\base : P(ze)) ⟶ (n : Nat) ⟶ P(n)```

This `elim-Nat` is the dependent elimination (induction) for the impredicatively defined natural numbers. I'm not sure one can manage to make the system typecheck `elim-Nat` using only the rules defined.