Domination and Levels

Due by 04 April 2014

For types $X$ and $Y$, define $Dominates(X)(Y):= \sum\limits_{f: X \to Y} \sum\limits_{g: Y \to X} f \circ g \sim id_Y$. If a term of this type exists we say $X$ dominates $Y$.

1. Prove (i.e., construct a term of type) $Dominates(X)(Y) \to isPropn(X) \to isPropn(Y)$.

2. Prove $Dominates(X)(Y) \to \prod\limits_{a, b: Y}\sum\limits_{c, d: X} Dominates(c = d)(a = b)$.

3. Suppose $X$ dominates $Y$. Conclude that if $X$ has level at most $n$ (where $n \geq -1$) then $Y$ has level at most $n$.