start

Rejestracja funktorowa

registration
  let x1 be Θ1;
   .....
  let xn be Θn;
  cluster τ(x1,...,xn) -> ξ1 ... ξm;
  coherence
  proof      :: thesis: τ(x1,...,xn) is ξ1 ... ξm
    thus τ(x1,...,xn)  is ξ1;
      ....
    thus τ(x1,...,xn)  is ξm;
  end;
end;

gdzie ξ₁, ..., ξ_m są przymiotnikami, do których typów definiowalności rozszerza się typ termu τ(x₁,...,x_n). Przymiotnik ξ_i może mieć argumenty jawne (τ_i,1,...,τ_i,ni) zależne od x₁,...,x_n.

Rejestracja powoduje automatyczne dołączanie przymiotników ξ₁(τ₁,...,τ_n), ..., ξ_m(τ₁,...,τ_n) do typu termu τ(τ₁,...,τ_n).

Wariant z zawężeniem typu:

registration
  let x1 be Θ1;
   .....
  let xn be Θn;
  cluster τ(x1,...,xn) -> ξ1 ... ξm for Θ(x1,...,xn);
  coherence
  proof      :: thesis: for x being Θ st x = τ(x1,...,xn)
                ::            holds x is ξ1 ... ξm
    let x be Θ;
    assume x = τ(x1,...,xn) ;
    thus x is ξ1;
      ....
    thus x is ξm;
  end;
end;

gdzie ξ₁, ..., ξ_m są przymiotnikami, do których typów definiowalności rozszerza się Θ(x₁,...,x_n) oraz Θ(x₁,...,x_n) rozszerza się do typy termu τ(x₁,...,x_n).