controlled_fix.md

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

Γ, x : %self(x). T,
  eq : %self(eq). (P : T -> Type) -> P (%unroll x) -> P M |- M : T[x := M]
--------------------------------------------------------------------------
%fix(self%x : T, eq). M : %self(x). T

Γ |- M : %self(x). T
---------------------
%unroll M : T[x := M]

---------------------------------------------------
%unroll (%fix(self%x : T, eq). M) ===
M[x := %fix(self%x : T, eq). M]
 [eq := %fix(eq, _). (P : T -> Type) => (x : P M) => x]


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

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