kewerson_self.md

Γ, x : %self(x). T |- T : Type
------------------------------
%self(x). T : Type

fix%Unit (unit : %self(unit). %unroll Unit unit unit) (u : %self(u). %unroll Unit unit u)
  = (P : (u : %self(u). %unroll Unit unit u) -> Type) -> P unit -> P u;
fix%unit : %unroll Unit unit unit = P => x => x;

Unit = %self(u). %unroll Unit unit u;
unit : Unit = unit;
ind (u : Unit) = %unroll u;

%fix(Unit)
Unit : %self(Unit).
  (unit : %self(unit). %unroll Unit unit unit) ->
  (u : %self(u). %unroll Unit unit u) -> Type


received : %self(k). %unroll Unit k k // unit := k; u := k
expected : %self(k). %unroll Unit k k // unit := k; u := k

%self. (%self. %unroll 1 0 0) -> (%self. %unroll 2 1 0) -> Type

%self. %unroll (1 : %self. (%self. %unroll 1 0 0) -> (%self. %unroll 2 1 0) -> Type) 0 0
%self. (%unroll 1 : (%self. %unroll 2 0 0) -> (%self. %unroll 3 1 0) -> Type) 0 0
%self. (%unroll 1 (0 : %self. %unroll 2 0 0) : (%self. %unroll 2 0 0) -> Type) 0
%self. (%unroll 1 0 0 : Type)