unit_using_self.m

```rust
// rules
// Those rules are fully church-style
Γ, x : A |- B : Type
---------------------------
Γ |- @self(x : A). B : Type

Γ, x : A |- M : B[x := @fix(x : A). M]  Γ |- A ≂ @self(x : A). B
----------------------------------------------------------------
Γ |- @fix(x : A). M : @self(x : A). B

Γ |- M : @self(x : A). B 
--------------------------
Γ |- @unroll M : B[x := M]

/*
3 general steps

Describe the type indexed by the constructors of the type
Make the type family itself
Close the family on the constructors

The following code assumes implicit unroll
*/

// shape of family, induction-induction required
T_P_Unit : Type;
T_p_unit : (P_Unit : T_P_Unit) -> Type;

T_P_Unit = @self(P_Unit : T_P_Unit). (p_unit : T_p_unit P_Unit) -> Type;
T_p_unit P_Unit = @self(p_unit : T_p_unit P_Unit). P_Unit p_unit;

// proto Unit
P_Unit : T_Unit;
p_unit : T_p_unit P_unit;

P_Unit p_unit = @self(u : P_Unit p_unit).
  (P : P_Unit p_unit -> Type) -> P p_unit -> P u;
p_unit = @fix(p_unit). P => (x : P p_unit) => x;

// closing
Unit = P_Unit p_unit;
unit : Unit = p_unit;
```