$ n y a nya ⎣⎢⎡ <?? ??? ??= ⎦⎥⎤ $ $Figure 2. A typical call matrix$

Call matrix is a technique used in the minimal

foetuslanguage to determine whether a program terminates in a predictable way. In short, a recursive call, i.e. a call from a function to itself would terminate if (but not only if) the callreducesat least one of the arguments, that is, the arguments is eliminated by pattern matching, projecting or applying. One program terminates, if all calls in it terminates. (Nov 27, 2020)

$Γ⊢Π(n:Y).A(n):UΓ⊢Y:UΓ,n:Y⊢A(n):U $ $Γ⊢(λn.a):Π(n:Y).A(n)Γ,n:Y⊢a:A(n) $ $Γ⊢Σ(n:Y).A(n):UΓ⊢Y:UΓ,n:Y⊢A(n):U $ $Γ⊢(n,a):Σ(n:Y).A(n)Γ⊢n:YΓ⊢a:A(n) $ $Γ⊢n=_{Y}a:UΓ⊢Y:UΓ⊢n,a:Y $ $Γ⊢refl_{n}:n=_{Y}nΓ⊢n:Y $

$Figure 1. Several deduction rulesof the Martin-Lo¨f type theory$

Martin-Löf type theory is the dependently typed lambda calculus equipped with the infamous $Id$ type, which is the

type of identity, or equality, given that it is an equivalence and satisfies the Leibniz property. This type is used as a basis of thepathin the originalhomotopy type theory, but the focus has moved to one constructive interpretation of the HoTT, namely thecubical type theory, where a path is indeed a function $p:[0,1]→A$. (Aug 17, 2020)